EVERY : tactic list -> tactic

SYNOPSIS

Sequentially applies all the tactics in a given list of tactics.

DESCRIPTION

When applied to a list of tactics [t1; ... ;tn], and a goal g, the tactical EVERY applies each tactic in sequence to every subgoal generated by the previous one. This can be represented as:

   EVERY [t1;...;tn] = t1 THEN ... THEN tn

If the tactic list is empty, the resulting tactic has no effect.

FAILURE CONDITIONS

The application of EVERY to a tactic list never fails. The resulting tactic fails iff any of the component tactics do.

COMMENTS

It is possible to use EVERY instead of THEN, but probably stylistically inferior. EVERY is more useful when applied to a list of tactics generated by a function.

SEE ALSO

FIRST, MAP_EVERY, THEN.