DISCH_TAC : tactic

SYNOPSIS
Moves the antecedent of an implicative goal into the assumptions.

DESCRIPTION
    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 CONDITIONS
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.

SEE ALSO
DISCH, DISCH_ALL, DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC.