enth
proofManagerLib.enth : tactic -> int -> proof
Applies a tactic to one goal, referenced by number, in the current goal list, replacing that goal with the resulting subgoals.
enth tac i applies tac to all the i'th goal in the current goal
list, replacing that goal in the goal list with the subgoals produced by
tac. It is an abbreviation for expand_list (NTH_GOAL tac i).
For interactively constructing suitable compound tactics, for example to test whether a particular subgoal can be proved easily, before attacking the other subgoals.
See also
proofManagerLib.expand_list,
proofManagerLib.elt,
Tactical.NTH_GOAL,
proofManagerLib.set_goal,
proofManagerLib.r