ALL_TAC
Tactical.ALL_TAC : tactic
Passes on a goal unchanged.
ALL_TAC applied to a goal g simply produces the subgoal list [g].
It is the identity for the THEN tactical.
Failure
Never fails.
Example
The tactic
INDUCT_THEN numTheory.INDUCTION THENL [ALL_TAC, tac]
applied to a goal g, applies INDUCT_THEN numTheory.INDUCTION to g
to give a basis and step subgoal; it then returns the basis unchanged,
along with the subgoals produced by applying tac to the step.
Used to write tacticals such as REPEAT. Also, it is often used as a
place-holder in building compound tactics using tacticals such as
THENL.
See also
Prim_rec.INDUCT_THEN,
Tactical.NO_TAC,
Tactical.REPEAT,
Tactical.THENL