----------------------------------------------------------------------
NTH_GOAL                                                    (Tactical)
----------------------------------------------------------------------
NTH_GOAL : tactic -> int -> list_tactic

SYNOPSIS
The list-tactic which applies a tactic to the
{n}’th member of a list of goals.

KEYWORDS
tactical.

DESCRIBE
If {tac} is a tactic, {NTH_GOAL n tac} is a
list-tactic which applies the tactic {tac} to the
{n}’th member of a list of goals.

Note that in the interactive system,
subgoals are printed in reverse order of their numbering.

FAILURE
The application of {NTH_GOAL} to a tactic and integer never fails.
The resulting list-tactic fails if {n} is less than 1 or greater than the
length of the goal list,
or finally if {tac} fails when applied to the {n}’th member of the goal list.

USES
Applying a tactic to a particular subgoal.

EXAMPLE
Where {tac1} and {tac2} are tactics, {tac1 THEN_LT NTH_GOAL n tac2}
applies {tac1} to a goal, and then applies {tac2} to the {n}’th resulting
subgoal.

SEEALSO
Tactical.THEN_LT, Tactical.THEN1, Tactical.HEADGOAL,
Tactical.LASTGOAL.

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