1\DOC AP_TERM_TAC 2 3\TYPE {AP_TERM_TAC : tactic} 4 5\SYNOPSIS 6Strips a function application from both sides of an equational goal. 7 8\LIBRARY 9bool 10 11\STRUCTURE 12Tactic 13 14\KEYWORDS 15tactic. 16 17\DESCRIBE 18{AP_TERM_TAC} reduces a goal of the form {A ?- f x = f y} by stripping away 19the function applications, giving the new goal {A ?- x = y}. 20{ 21 A ?- f x = f y 22 ================ AP_TERM_TAC 23 A ?- x = y 24} 25 26 27\FAILURE 28Fails unless the goal is equational, with both sides being applications 29of the same function. 30 31\SEEALSO 32Thm.AP_TERM, Thm.AP_THM, Tactic.AP_THM_TAC, Tactic.MK_COMB_TAC, Tactic.ABS_TAC. 33 34\ENDDOC 35