ALL_TAC : tactic
STRUCTURE
Tactical
SYNOPSIS
Passes on a goal unchanged.
DESCRIPTION
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
INDUCT_THEN, NO_TAC, REPEAT, THENL
HOL  Kananaskis-14