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