----------------------------------------------------------------------
THEN_LT                                                     (Tactical)
----------------------------------------------------------------------
op THEN_LT : tactic * list_tactic -> tactic
op THEN_LT : list_tactic * list_tactic -> list_tactic

SYNOPSIS
Applies a list-tactic to the corresponding subgoals generated by a tactic
or by a previous list-tactic.

KEYWORDS
tactical, list-tactic.

DESCRIBE
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
Tactical.ALLGOALS, Tactical.THEN, Tactical.TACS_TO_LT, Tactical.THENL,
Tactical.NULL_OK_LT, Tactical.NTH_GOAL, Tactical.REVERSE_LT,
Tactical.REVERSE.

----------------------------------------------------------------------