ACL2-PC::NEGATE

(macro) run the given instructions, and ``succeed'' if and only if they ``fail''
Major Section:  PROOF-CHECKER-COMMANDS

Example: (negate prove)

General form:
(negate &rest instruction-list)
Run the indicated instructions exactly in the sense of do-all, and ``succeed'' if and only if they ``fail''.

Remark: Negate instructions will never produce hard ``failures''.