ACL2-PC::DO-STRICT

(macro) run the given instructions, halting once there is a ``failure''
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(do-strict induct p prove)

General Form:
(do-strict &rest instruction-list)
Run the indicated instructions until there is a (hard or soft) ``failure''. In fact 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.