1\DOC ABS_TAC
2
3\TYPE {ABS_TAC : tactic}
4
5\SYNOPSIS
6Strips lambda abstraction on both sides of an equation.
7
8\LIBRARY
9bool
10
11\STRUCTURE
12Tactic
13
14\KEYWORDS
15tactic.
16
17\DESCRIBE
18When applied to a goal of the form {A ?- (\x. f x) = (\y. g u)}, the tactic {ABS_TAC}
19strips away the lambda abstractions:
20{
21    A ?- (\x. f x) = (\y. g y)
22   ===========================  ABS_TAC
23            A ?- f x = g x
24}
25
26
27\FAILURE
28Fails unless the goal has the above form, namely an equation both sides of
29which consist of a lamdba abstraction.
30
31\SEEALSO
32Tactic.AP_TERM_TAC, Tactic.AP_THM_TAC.
33\ENDDOC
34