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