ACL2-PC::REPEAT

(macro) repeat the given instruction until it ``fails''
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(repeat promote)

General Form:
(repeat instruction)
The given instruction is 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.