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)`