AP_TERM

Thm.AP_TERM : term -> thm -> thm

Applies a function to both sides of an equational theorem.

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.

See also

Tactic.AP_TERM_TAC, Thm.AP_THM, Tactic.AP_THM_TAC, Thm.MK_COMB