REPEAT

Tactical.REPEAT : (tactic -> tactic)

Repeatedly applies a tactic until it fails.

The tactic REPEAT T is a tactic which applies T to a goal, and while it succeeds, continues applying it to all subgoals generated.

Failure

The application of REPEAT to a tactic never fails, and neither does the composite tactic, even if the basic tactic fails immediately.

See also

Tactical.EVERY, Tactical.FIRST, Tactical.ORELSE, Tactical.THEN, Tactical.THENL