DISJ_CASES_THEN : thm_tactical
A ?- t A ?- t ========= f (u |- u) and ========= f (v |- v) A ?- t1 A ?- t2
A ?- t ====================== DISJ_CASES_THEN f (|- u \/ v) A ?- t1 A ?- t2
th = |- (m = 0) \/ (?n. m = SUC n)
DISJ_CASES_THEN MP_TAC th
# let th = SPEC `m:num` num_CASES;; val th : thm = |- m = 0 \/ (?n. m = SUC n) # g `PRE m = m <=> m = 0`;; Warning: Free variables in goal: m val it : goalstack = 1 subgoal (1 total) `PRE m = m <=> m = 0` # e(DISJ_CASES_THEN MP_TAC th);; val it : goalstack = 2 subgoals (2 total) `(?n. m = SUC n) ==> (PRE m = m <=> m = 0)` `m = 0 ==> (PRE m = m <=> m = 0)`
let DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC