ALL_TAC applied to a goal g simply produces the subgoal list [g]. It is
the identity for the THEN tactical.
Suppose we want to solve the goal:
# g `~(n MOD 2 = 0) <=> n MOD 2 = 1`;;
We could just solve it with e ARITH_TAC, but suppose we want to introduce a
little lemma that n MOD 2 < 2, proving that by ARITH_TAC. We could do
# e(SUBGOAL_THEN `n MOD 2 < 2` ASSUME_TAC THENL
...rest of proof...]);;
However if we split off many lemmas, we get a deeply nested proof structure
that's a bit confusing. In cases where the proofs of the lemmas are trivial
one-liners like this we might just want to keep the proof basically linear with
# e(SUBGOL_THEN `n MOD 2 < 2` ASSUME_TAC THENL [ARITH_TAC; ALL_TAC] THEN
...rest of proof...);;
Keeping proof structures linear, as in the above example, or convenient
algebraic combinations in complicated tactic structures.