AP_TERM : term -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Applies a function to both sides of an equational theorem.
DESCRIPTION
When applied to a term f and a theorem A |- x = y, the inference rule AP_TERM returns the theorem A |- f x = f y. 
      A |- x = y
   ----------------  AP_TERM f
    A |- f x = f y

FAILURE
Fails unless the theorem is equational and the supplied term is a function whose domain type is the same as the type of both sides of the equation.
SEEALSO
AP_TERM_TAC, AP_THM, AP_THM_TAC, MK_COMB
HOL  Trindemossen-1