MK_PABS : (thm -> thm)
STRUCTURE
LIBRARY
pair
SYNOPSIS
Abstracts both sides of an equation.
DESCRIPTION
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
HOL  Trindemossen-1