op THEN_LT : tactic * list_tactic -> tactic op THEN_LT : list_tactic * list_tactic -> list_tactic

- STRUCTURE
- SYNOPSIS
- Applies a list-tactic to the corresponding subgoals generated by a tactic or by a previous list-tactic.
- DESCRIPTION
- 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.

- USES
- 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

- SEEALSO

HOL Kananaskis-13