ABS_TAC : tactic
SYNOPSIS
Strips lambda abstraction on both sides of an equation.
LIBRARY
bool
STRUCTURE
DESCRIPTION
When applied to a goal of the form A ?- (\x. f x) = (\y. g u), the tactic ABS_TAC strips away the lambda abstractions:
    A ?- (\x. f x) = (\y. g y)
   ===========================  ABS_TAC
            A ?- f x = g x

FAILURE
Fails unless the goal has the above form, namely an equation both sides of which consist of a lamdba abstraction.
SEEALSO
HOL  Trindemossen-1