The list-tactic which applies a tactic to the last member of a list of goals.
DESCRIPTION
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.
FAILURE
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.
USES
Applying a tactic to the last subgoal.
EXAMPLE
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.