DESTRUCT_TAC : string -> thm_tactic
# let th = SPEC `n:num` (cases "num");; # g `n = 0 \/ (1 <= n /\ ?m. n = m + 1)`;; # e (DESTRUCT_TAC "neq0 | @m. neqsuc" th);; val it : goalstack = 2 subgoals (2 total) 0 [`n = SUC m`] (neqsuc) `n = 0 \/ 1 <= n /\ (?m. n = m + 1)` 0 [`n = 0`] (neq0) `n = 0 \/ 1 <= n /\ (?m. n = m + 1)`
# let th = SPEC `n+2` EVEN_EXISTS_LEMMA;; val th : thm = |- (EVEN (n + 2) ==> (?m. n + 2 = 2 * m)) /\ (~EVEN (n + 2) ==> (?m. n + 2 = SUC (2 * m)))
# g `!n. ~EVEN n ==> ?a. n + 2 = 2 * a + 1`;; # e (REPEAT STRIP_TAC THEN DESTRUCT_TAC "_ +" th);; val it : goalstack = 1 subgoal (1 total) 0 [`~EVEN n`] `(~EVEN (n + 2) ==> (?m. n + 2 = SUC (2 * m))) ==> (?a. n + 2 = 2 * a + 1)`