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.