ALL_LT : list_tactic
STRUCTURE
Tactical
SYNOPSIS
Passes on a goal list unchanged.
DESCRIPTION
ALL_LT applied to a goal list gl simply produces the goal list gl. It is the identity for the THEN_LT tactical.
FAILURE
Never fails.
EXAMPLE
To apply tactic tac1 to a goal, and then to apply tac2 to all resulting subgoals except the first, use 
  tac1 THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS tac2)
SEEALSO
THEN_LT, SPLIT_LT, ALLGOALS
HOL  Kananaskis-14