1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
\DOC AP_THM_TAC
\TYPE {AP_THM_TAC : tactic}
\SYNOPSIS
Strips identical operands from functions on both sides of an equation.
\KEYWORDS
tactic.
\DESCRIBE
When applied to a goal of the form {A ?- f x = g x}, the tactic {AP_THM_TAC}
strips away the operands of the function application:
{
A ?- f x = g x
================ AP_THM_TAC
A ?- f = g
}
\FAILURE
Fails unless the goal has the above form, namely an equation both sides of
which consist of function applications to the same argument.
\SEEALSO
ABS_TAC, AP_TERM_TAC, AP_THM, BINOP_TAC, MK_COMB_TAC.
\ENDDOC
|
