UNDISCH_ALL : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Iteratively undischarges antecedents in a chain of implications.
DESCRIPTION
    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.
SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, NEG_DISCH, FILTER_DISCH_TAC, FILTER_DISCH_THEN, STRIP_TAC, UNDISCH, UNDISCH_TAC
HOL  Kananaskis-14