UNDISCH_SPLIT

Drule.UNDISCH_SPLIT : thm -> thm

Undischarges the antecedent of an implicative theorem, and splits it into its conjuncts.

    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.

See also

Thm.DISCH, Drule.DISCH_ALL, Tactic.DISCH_TAC, Thm_cont.DISCH_THEN, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Drule.NEG_DISCH, Tactic.STRIP_TAC, Drule.UNDISCH, Drule.UNDISCH_ALL, Drule.UNDISCH_TM, Tactic.UNDISCH_TAC, Drule.ASSUME_CONJS