REPEAT : (tactic -> tactic)
STRUCTURE
Tactical
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
EVERY
,
FIRST
,
ORELSE
,
THEN
,
THENL
HOL
Kananaskis-14