SIMPLE_DISJ_CASES : thm -> thm -> thm
A u {p} |- r B u {q} |- r ----------------------------------------- SIMPLE_DISJ_CASES (A - {p}) u (B - {q}) u {p \/ q} |- r
{p} |- r {q} |- r ---------------------------- SIMPLE_DISJ_CASES {p \/ q} |- r
# let [th1; th2] = map (UNDISCH o TAUT) [`~p ==> p ==> q`; `q ==> p ==> q`];; ... val th1 : thm = ~p |- p ==> q val th2 : thm = q |- p ==> q # SIMPLE_DISJ_CASES th1 th2;; val it : thm = ~p \/ q |- p ==> q