DISJ_CASES_THEN2 : thm_tactic -> thm_tactic -> thm_tactic
A ?- t A ?- t ========= ttac1 (u |- u) and ========= ttac2 (v |- v) A ?- t1 A ?- t2
A ?- t ====================== DISJ_CASES_THEN2 ttac1 ttac2 (|- u \/ v) A ?- t1 A ?- t2
# let th = SPEC `m:num` num_CASES;; val th : thm = |- m = 0 \/ (?n. m = SUC n)
# g `PRE m = m <=> m = 0`;;
# e(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC th);; val it : goalstack = 2 subgoals (2 total) `(?n. m = SUC n) ==> (PRE m = m <=> m = 0)` `PRE 0 = 0 <=> 0 = 0`
# e(DISJ_CASES_THEN2 SUBST1_TAC (CHOOSE_THEN SUBST1_TAC) th);; val it : goalstack = 2 subgoals (2 total) `PRE (SUC n) = SUC n <=> SUC n = 0` `PRE 0 = 0 <=> 0 = 0`
let DISJ_CASES_THEN f = DISJ_CASES_THEN2 f f