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 Kananaskis-14