UNDISCH : thm -> thm
STRUCTURE
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
HOL  Kananaskis-13