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