		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::insist-all-proved

(macro) Run the given instructions, then fail if there remain unproved goals

Example:
(insist-all-proved (succeed bash) induct (repeat prove))

General Form:
(insist-all-proved instr1 ... instrk)

where each instri is a proof-builder instruction.

Run the given instructions until one fails, as with the :do-strict command. The call of :insist-all-proved succeeds only when none of those instructions fails and, moreover, all goals are proved when the instructions complete.