ACL2-PC::DO-ALL

(macro) run the given instructions 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(do-all induct p prove)


General Form:
(do-all &rest instruction-list)
Run the indicated instructions until there is a hard ``failure''. The instruction ``succeeds'' if and only if each instruction in instruction-list does. (See the documentation for sequence for an explanation of ``success'' and ``failure.'') As each instruction is executed, the system will print the usual prompt followed by that instruction, unless the global state variable print-prompt-and-instr-flg is nil.

Note: If do-all ``fails'', then the failure is hard if and only if the last instruction it runs has a hard ``failure''.

Obscure point: For the record, (do-all ins_1 ins_2 ... ins_k) is the same as (sequence (ins_1 ins_2 ... ins_k)).