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
pc-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))
.