The list-tactic which applies a tactic to the
n’th member of a list of goals.
DESCRIPTION
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.