1\DOC AP_THM_TAC 2 3\TYPE {AP_THM_TAC : tactic} 4 5\SYNOPSIS 6Strips identical operands from functions 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 ?- f x = g x}, the tactic {AP_THM_TAC} 19strips away the operands of the function application: 20{ 21 A ?- f x = g x 22 ================ AP_THM_TAC 23 A ?- f = g 24} 25 26 27\FAILURE 28Fails unless the goal has the above form, namely an equation both sides of 29which consist of function applications to the same arguments. 30 31\SEEALSO 32Thm.AP_TERM, Tactic.AP_TERM_TAC, Thm.AP_THM, Tactic.MK_COMB_TAC, 33Tactic.ABS_TAC, Drule.EXT. 34\ENDDOC 35