DISJ_CASES_TAC : thm_tactic
A ?- t ================================= DISJ_CASES_TAC (A |- u \/ v) A u {u} ?- t A u {v}?- t
# let th = SPEC `m:num` num_CASES;; val th : thm = |- m = 0 \/ (?n. m = SUC n) # g `(P:num -> bool) m`;; Warning: Free variables in goal: P, m val it : goalstack = 1 subgoal (1 total) `P m` # e(DISJ_CASES_TAC th);; val it : goalstack = 2 subgoals (2 total) 0 [`?n. m = SUC n`] `P m` 0 [`m = 0`] `P m`