AP_TERM : term -> thm -> thm

- STRUCTURE
- 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

HOL Kananaskis-14