DISJ_CASES_UNION : thm -> thm -> thm -> thm
STRUCTURE
Drule
SYNOPSIS
Makes an inference for each arm of a disjunct.
DESCRIPTION
Given a disjunctive theorem, and two additional theorems each having one disjunct as a hypothesis, a new theorem with a conclusion that is the disjunction of the conclusions of the last two theorems is produced. The hypotheses include the union of hypotheses of all three theorems less the two disjuncts. 
    A |- t1 \/ t2    A1 u {t1} |- t3     A2 u {t2} |- t4
   ------------------------------------------------------  DISJ_CASES_UNION
                 A u A1 u A2 |- t3 \/ t4

FAILURE
Fails if the first theorem is not a disjunction.
EXAMPLE
The built-in theorem LESS_CASES can be specialized to: 
   th1 = |- m < n \/ n <= m
and used with two additional theorems: 
   th2 = (m < n |- (m MOD n = m))
   th3 = ({0 < n, n <= m} |- (m MOD n) = ((m - n) MOD n))
to derive a new theorem: 
   - DISJ_CASES_UNION th1 th2 th3;
   val it = [0 < n] |- (m MOD n = m) \/ (m MOD n = (m - n) MOD n) : thm

SEEALSO
DISJ_CASES, DISJ_CASES_TAC, DISJ1, DISJ2
HOL  Kananaskis-13