DISCH_TAC : tactic
STRUCTURE
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
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, FILTER_DISCH_TAC, FILTER_DISCH_THEN, NEG_DISCH, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC
HOL  Kananaskis-13