HEADGOAL

Tactical.HEADGOAL : tactic -> list_tactic

The list-tactic which applies a tactic to the first member of a list of goals.

If tac is a tactic, HEADGOAL tac is a list-tactic which applies the tactic tac to the first member of a list of goals.

Failure

The application of HEADGOAL 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 first member of the goal list.

Applying a tactic to the first subgoal.

Example

Where tac1 and tac2 are tactics, tac1 THEN_LT HEADGOAL tac2 applies tac1 to a goal, and then applies tac2 to the first resulting subgoal.

See also

Tactical.THEN_LT, Tactical.NTH_GOAL, Tactical.THEN1, Tactical.LASTGOAL