PABS : (term -> thm -> thm)
STRUCTURE
PairRules
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
ABS, PABS_CONV, PETA_CONV, PEXT, MK_PABS
HOL  Kananaskis-13