TACS_TO_LTTactical.TACS_TO_LT : tactic list -> list_tacticThe list-tactic which applies a list of tactics to the corresponding members of a list of goals.
If T1,...,Tn are tactics,
TACS_TO_LT [T1,...,Tn] is a list-tactic which applies the
tactics T1,...,Tn to the corresponding goals.
The application of TACS_TO_LT to a tactic list never
fails. The resulting list-tactic fails if length of the goal list is not
the same as that of the tactic list, or finally if Ti fails
when applied to the i’th member of the goal list.
Applying different tactics to different subgoals.
Where tac1 is a tactic and tacs2 is a list
of tactics, tac1 THEN_LT TACS_TO_LT tacs2 is equivalent to
tac1 THENL tacs2