TRYALL
Tactical.TRYALL : tactic -> list_tactic
Tries to apply a tactic to every goal in a list
If tac is a tactic, TRYALL tac is a list-tactic which, when applied
to a list of goals, applies the tactic tac to each goal for which it
succeeds. When tac fails on a goal, TRYALL tac has no effect on that
goal.
Failure
The application of TRYALL to a tactic never fails. The resulting
list-tactic never fails.
Example
Where tac1 and tac2 are tactics, tac1 THEN_LT TRYALL tac2 is
equivalent to tac1 THEN TRY tac2
See also
Tactical.TRY,
Tactical.THEN_LT,
Tactical.THEN, Tactical.TRY,
Tactical.ALLGOALS