UNDISCH_ALL

Drule.UNDISCH_ALL : thm -> thm

Iteratively undischarges antecedents in a chain of implications.

    A |- t1 ==> ... ==> tn ==> t
   ------------------------------  UNDISCH_ALL
        A, t1, ..., tn |- t

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

Failure

UNDISCH_ALL never fails. When called on something other than an implication or negation, it simply returns its argument unchanged.

Comments

Identical or alpha-equivalent terms which are repeated in A, "t1", ..., "tn" will not be duplicated in the hypotheses of the resulting theorem.

See also

Thm.DISCH, Drule.DISCH_ALL, Tactic.DISCH_TAC, Thm_cont.DISCH_THEN, Drule.NEG_DISCH, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Tactic.STRIP_TAC, Drule.UNDISCH, Tactic.UNDISCH_TAC