----------------------------------------------------------------------
ALL_TAC                                                     (Tactical)
----------------------------------------------------------------------
ALL_TAC : tactic

SYNOPSIS
Passes on a goal unchanged.

KEYWORDS
tactic, identity.

DESCRIBE
{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.

USES
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}.

SEEALSO
Prim_rec.INDUCT_THEN, Tactical.NO_TAC, Tactical.REPEAT,
Tactical.THENL.

----------------------------------------------------------------------