UNDISCH_SPLIT : thm -> thm
STRUCTURE
Drule
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
DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_TAC, FILTER_DISCH_THEN, NEG_DISCH, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TM, UNDISCH_TAC, ASSUME_CONJS
HOL  Kananaskis-14