ACL2-pc::do-all-no-prompt
(macro)
run the given instructions, halting once there is a ``failure''
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
pc-print-prompt-and-instr-flg. Also, restoring is disabled. See ACL2-pc::do-all.
