run the given instructions, halting once there is a ``failure''
Major Section: PROOF-CHECKER-COMMANDS
Example: (do-strict induct p prove)Run the indicated instructions until there is a (hard or soft) ``failure''. In factGeneral Form: (do-strict &rest instruction-list)
do-strict
is identical in effect to do-all
,
except that do-all
only halts once there is a hard ``failure''. See
the documentation for do-all
.