UNDISCH

Drule.UNDISCH : thm -> thm

Undischarges the antecedent of an implicative theorem.

    A |- t1 ==> t2
   ----------------  UNDISCH
     A, t1 |- t2

Note that UNDISCH treats "~u" as "u ==> F".

Failure

UNDISCH will fail on theorems which are not implications or negations.

Comments

If the antecedent already appears in (or is alpha-equivalent to one of) the hypotheses, it will not be duplicated.

See also

Thm.DISCH, Drule.DISCH_ALL, Tactic.DISCH_TAC, Thm_cont.DISCH_THEN, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Drule.NEG_DISCH, Tactic.STRIP_TAC, Drule.UNDISCH_ALL, Drule.UNDISCH_SPLIT, Drule.UNDISCH_TM, Tactic.UNDISCH_TAC