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.
The application of REPEAT to a tactic never fails, and neither does the
composite tactic, even if the basic tactic fails immediately.