LASTGOALTactical.LASTGOAL : tactic -> list_tacticThe list-tactic which applies a tactic to the last member of a list of goals.
If tac is a tactic, LASTGOAL tac is a
list-tactic which applies the tactic tac to the last member
of a list of goals.
The application of LASTGOAL to a tactic never fails. The
resulting list-tactic fails the goal list is empty or or finally if
tac fails when applied to the last member of the goal
list.
Applying a tactic to the last subgoal.
Where tac1 and tac2 are tactics,
tac1 THEN_LT LASTGOAL tac2 applies tac1 to a
goal, and then applies tac2 to the last resulting
subgoal.