----------------------------------------------------------------------
DISCH_TAC                                                     (Tactic)
----------------------------------------------------------------------
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

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
Thm.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.

----------------------------------------------------------------------