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_TERM_TAC
\TYPE {AP_TERM_TAC : tactic}
\SYNOPSIS
Strips a function application from both sides of an equational goal.
\KEYWORDS
tactic.
\DESCRIBE
{AP_TERM_TAC} reduces a goal of the form {A ?- f x = f y} by stripping away
the function applications, giving the new goal {A ?- x = y}.
{
A ?- f x = f y
================ AP_TERM_TAC
A ?- x = y
}
\FAILURE
Fails unless the goal is equational, with both sides being applications
of the same function.
\SEEALSO
ABS_TAC, AP_TERM, AP_THM_TAC, BINOP_TAC, MK_COMB_TAC.
\ENDDOC
|
