THEN_LTop Tactical.THEN_LT : tactic * list_tactic -> tactic
op THEN_LT : list_tactic * list_tactic -> list_tacticApplies a list-tactic to the corresponding subgoals generated by a tactic or by a previous list-tactic.
If tac is a tactic and ltac is a
list-tactic, then tac THEN_LT ltac is a tactic which
applies tac to a goal, and if it does not fail, applies the
list-tactic ltac to the resulting list of subgoals.
If ltac1 and ltac2 are list-tactics, then
ltac1 THEN_LT ltac2 is a list-tactic which applies
ltac1 to a goal list, and if it does not fail, applies
ltac2 to the resulting list of goals.
The application of THEN_LT to a tactic or list-tactic
and a list-tactic never fails.
The tactic tac THEN_LT ltac fails if tac
fails when applied to the goal, or if ltac fails when
applied to the resulting subgoal list.
The list-tactic ltac1 THEN_LT ltac2 fails if
ltac1 fails when applied to the goal list, or if
ltac2 fails when applied to the goal list result of
ltac1.
Applying a combination of tactics to a list of subgoals, or otherwise manipulating a list of subgoals.
Where tac1 and tac2 are tactics,
tac1 THEN_LT ALLGOALS tac2 is equivalent to
tac1 THEN tac2
Where tac1 is a tactic and tacs2 is a list
of tactics, tac1 THEN_LT NULL_OK_LT (TACS_TO_LT tacs2) is
equivalent to tac1 THENL tacs2
Where tac is a tactic,
tac THEN_LT REVERSE_LT is equivalent to
REVERSE tac
Tactical.ALLGOALS,
Tactical.THEN, Tactical.TACS_TO_LT, Tactical.THENL, Tactical.NULL_OK_LT, Tactical.NTH_GOAL, Tactical.REVERSE_LT, Tactical.REVERSE