UNDISCH : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Undischarges the antecedent of an implicative theorem.
DESCRIPTION
    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.
SEEALSO
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, FILTER_DISCH_THEN, NEG_DISCH, STRIP_TAC, UNDISCH_ALL, UNDISCH_SPLIT, UNDISCH_TM, UNDISCH_TAC
HOL  Kananaskis-13