DISJ_CASES : thm -> thm -> thm -> thm
A |- t1 \/ t2 A1 |- t A2 |- t -------------------------------------------------- DISJ_CASES A u (A1 - {t1}) u (A2 - {t2}) |- t
# let [th; th1; th2] = map (UNDISCH_ALL o REAL_FIELD) [`~(x = &0) \/ x = &0`; `~(x = &0) ==> x * (inv(x) * x - &1) = &0`; `x = &0 ==> x * (inv(x) * x - &1) = &0`];; ... val th : thm = |- ~(x = &0) \/ x = &0 val th1 : thm = ~(x = &0) |- x * (inv x * x - &1) = &0 val th2 : thm = x = &0 |- x * (inv x * x - &1) = &0
# DISJ_CASES th th1 th2;; val it : thm = |- x * (inv x * x - &1) = &0