op THENL : tactic * tactic list -> tactic
op THENL : list_tactic * tactic list -> list_tactic
STRUCTURE
Tactical
SYNOPSIS
Applies a list of tactics to the corresponding subgoals generated by a tactic or a list-tactic.
DESCRIPTION
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
EVERY, ORELSE, THEN, THEN_LT
HOL  Kananaskis-14