ABS : term -> thm -> thm
STRUCTURE
Thm
SYNOPSIS
Abstracts both sides of an equation.
DESCRIPTION
         A |- t1 = t2
   ------------------------  ABS x            [Where x is not free in A]
    A |- (\x.t1) = (\x.t2)

FAILURE
If the theorem is not an equation, or if the variable x is free in the assumptions A.
EXAMPLE
- let val m = Term `m:bool`
  in
      ABS m (REFL m)
  end;

> val it = |- (\m. m) = (\m. m) : thm
SEEALSO
ETA_CONV, EXT, MK_ABS
HOL  Trindemossen-1