ABS : term -> thm -> 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 CONDITIONS
If the theorem is not an equation, or if the variable x is free in the assumptions A.

EXAMPLE
  # ABS `m:num` (REFL `m:num`);;
  val it : thm = |- (\m. m) = (\m. m)

COMMENTS
This is one of HOL Light's 10 primitive inference rules.

SEE ALSO
ETA_CONV.