ACL2-PC::PROTECT

(macro) run the given instructions, reverting to existing state upon failure
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(protect induct p prove)

General Form: (protect &rest instruction-list)

Protect is the same as do-strict, except that as soon as an instruction ``fails'', the state-stack reverts to what it was before the protect instruction began, and restore is given the same meaning that it had before the protect instruction began. See the documentation for do-strict.