----------------------------------------------------------------------
MK_PABS                                                    (PairRules)
----------------------------------------------------------------------
MK_PABS : (thm -> thm)

KEYWORDS
rule, abstraction, equality.

LIBRARY
pair

SYNOPSIS
Abstracts both sides of an equation.

DESCRIBE
When applied to a theorem {A |- !p. t1 = t2}, whose conclusion is a
paired universally quantified equation, {MK_PABS} returns the theorem
{A |- (\p. t1) = (\p. t2)}.

        A |- !p. t1 = t2
   --------------------------  MK_PABS
    A |- (\p. t1) = (\p. t2)




FAILURE
Fails unless the theorem is a (singly) paired universally quantified equation.

SEEALSO
Drule.MK_ABS, PairRules.PABS, PairRules.HALF_MK_PABS,
PairRules.MK_PEXISTS.

----------------------------------------------------------------------