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