THEN_LT
op Tactical.THEN_LT : tactic * list_tactic -> tactic
op THEN_LT : list_tactic * list_tactic -> list_tactic
Applies 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.
Failure
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.
Example
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
See also
Tactical.ALLGOALS,
Tactical.THEN,
Tactical.TACS_TO_LT,
Tactical.THENL,
Tactical.NULL_OK_LT,
Tactical.NTH_GOAL,
Tactical.REVERSE_LT,
Tactical.REVERSE