1\DOC DISCH_TAC
2
3\TYPE {DISCH_TAC : tactic}
4
5\SYNOPSIS
6Moves the antecedent of an implicative goal into the assumptions.
7
8\KEYWORDS
9tactic, undischarge, antecedent, implication.
10
11\DESCRIBE
12{
13    A ?- u ==> v
14   ==============  DISCH_TAC
15    A u {u} ?- v
16}
17Note that {DISCH_TAC} treats {~u} as {u ==> F}, so will also work
18when applied to a goal with a negated conclusion.
19
20\FAILURE
21{DISCH_TAC} will fail for goals which are not implications or negations.
22
23\USES
24Solving goals of the form {u ==> v} by rewriting {v} with {u}, although
25the use of {DISCH_THEN} is usually more elegant in such cases.
26
27\COMMENTS
28If the antecedent already appears in the assumptions, it will be duplicated.
29
30\SEEALSO
31Thm.DISCH, Drule.DISCH_ALL, Thm_cont.DISCH_THEN, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Drule.NEG_DISCH, Tactic.STRIP_TAC, Drule.UNDISCH, Drule.UNDISCH_ALL, Tactic.UNDISCH_TAC.
32\ENDDOC
33