----------------------------------------------------------------------
THENL                                                       (Tactical)
----------------------------------------------------------------------
op THENL : tactic * tactic list -> tactic
op THENL : list_tactic * tactic list -> list_tactic

SYNOPSIS
Applies a list of tactics to the corresponding subgoals generated by a
tactic or a list-tactic.

KEYWORDS
tactical.

DESCRIBE
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}.

USES
Applying different tactics to different subgoals.

SEEALSO
Tactical.EVERY, Tactical.ORELSE, Tactical.THEN, Tactical.THEN_LT.

----------------------------------------------------------------------