ACL2-pc::protect
(macro)
run the given instructions, reverting to existing state upon
failure
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 ACL2-pc::do-strict.
