MK_PABS
PairRules.MK_PABS : (thm -> thm)
Abstracts both sides of an equation.
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.
See also
Drule.MK_ABS, PairRules.PABS,
PairRules.HALF_MK_PABS,
PairRules.MK_PEXISTS