MK_ABS : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Abstracts both sides of an equation.
DESCRIPTION
When applied to a theorem A |- !x. t1 = t2, whose conclusion is a universally quantified equation, MK_ABS returns the theorem A |- \x. t1 = \x. t2. 
        A |- !x. t1 = t2
   --------------------------  MK_ABS
    A |- (\x. t1) = (\x. t2)

FAILURE
Fails unless the theorem is a (singly) universally quantified equation.
SEEALSO
ABS, HALF_MK_ABS, MK_COMB, MK_EXISTS
HOL  Kananaskis-14