ACL2-pc::do-all
(macro)
run the given instructions
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 ACL2-pc::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 value of
(access pc-info (@ pc-info) :print-prompt-and-instr-flg) is nil.
Remark: 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)).
