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
28
29
30
31
32
33
|
\DOC DISCH_TAC
\TYPE {DISCH_TAC : tactic}
\SYNOPSIS
Moves the antecedent of an implicative goal into the assumptions.
\KEYWORDS
tactic, undischarge, antecedent, implication.
\DESCRIBE
{
A ?- u ==> v
============== DISCH_TAC
A u {{u}} ?- v
}
\noindent Note that {DISCH_TAC} treats {`~u`} as {`u ==> F`}, so will also work
when applied to a goal with a negated conclusion.
\FAILURE
{DISCH_TAC} will fail for goals which are not implications or negations.
\USES
Solving goals of the form {`u ==> v`} by rewriting {`v`} with {`u`}, although
the use of {DISCH_THEN} is usually more elegant in such cases.
\COMMENTS
If the antecedent already appears in the assumptions, it will be duplicated.
\SEEALSO
DISCH, DISCH_ALL, DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.
\ENDDOC
|
