PABS : (term -> thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Paired abstraction of both sides of an equation.
- DESCRIPTION
A |- t1 = t2 ------------------------ ABS "p" [Where p is not free in A] A |- (\p.t1) = (\p.t2)

- FAILURE
- If the theorem is not an equation, or if any variable in the paired structure of variables p occurs free in the assumptions A.
EXAMPLE

- PABS (Term `(x:'a,y:'b)`) (REFL (Term `(x:'a,y:'b)`)); > val it = |- (\(x,y). (x,y)) = (\(x,y). (x,y)) : thm

- SEEALSO

HOL Kananaskis-14