op THEN_LT : tactic * list_tactic -> tactic
op THEN_LT : list_tactic * list_tactic -> list_tactic
STRUCTURE
Tactical
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
ALLGOALS, THEN, TACS_TO_LT, THENL, NULL_OK_LT, NTH_GOAL, REVERSE_LT, REVERSE
HOL  Trindemossen-1