repeat the given instruction until it ``fails''
Major Section: PROOF-CHECKER-COMMANDS
Example: (repeat promote)The given
General Form: (repeat instruction)
instructionis run repeatedly until it ``fails''.
Remark: There is nothing here in general to prevent the instruction
from being run after all goals have been proved, though this is
indeed the case for primitive instructions.