ACL2-PC::DO-ALL-NO-PROMPT

(macro) run the given instructions, halting once there is a ``failure''
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(do-all-no-prompt induct p prove)

General Form: (do-all-no-prompt &rest instruction-list)

Do-all-no-prompt is the same as do-all, except that the prompt and instruction are not printed each time, regardless of the value of print-prompt-and-instr-flg. Also, restoring is disabled. See the documentation for do-all.