UNDISCH_SPLIT : thm -> thm
STRUCTURE
SYNOPSIS
Undischarges the antecedent of an implicative theorem, and splits it into its conjuncts.
DESCRIPTION
    A |- t1a /\ t1b /\ t1c ==> t2
   ------------------------------  UNDISCH_SPLIT
     A, t1a, t1b, t1c |- t2
Note that UNDISCH_SPLIT treats "~u" as "u ==> F".
FAILURE
UNDISCH_SPLIT will fail on theorems which are not implications or negations.
COMMENTS
If a conjunct of the antecedent already appears in (or is alpha-equivalent to one of) the hypotheses, it will not be duplicated.
SEEALSO
HOL  Trindemossen-1