REPEAT : (tactic -> tactic)
STRUCTURE
SYNOPSIS
Repeatedly applies a tactic until it fails.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1