THENL
op Tactical.THENL : tactic * tactic list -> tactic
op THENL : list_tactic * tactic list -> list_tactic
Applies a list of tactics to the corresponding subgoals generated by a tactic or a list-tactic.
If T is a tactic or list-tactic and T1,...,Tn are tactics,
T THENL [T1,...,Tn] is a tactic or list-tactic which applies T to a
goal or goal list, and if it does not fail, applies the tactics
T1,...,Tn to the corresponding subgoals, unless T completely solves
the goal(s).
Failure
The application of THENL to a (list-)tactic and tactic list never
fails. The resulting tactic fails if T fails when applied to the
goal(s), or if the goal list is not empty and its length is not the same
as that of the tactic list, or finally if Ti fails when applied to the
i'th subgoal generated by T.
Applying different tactics to different subgoals.
See also
Tactical.EVERY,
Tactical.ORELSE,
Tactical.THEN,
Tactical.THEN_LT