ACL2-PC::ORELSE

(macro) run the first instruction; if (and only if) it ``fails'', run the second
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(orelse top (print "Couldn't move to the top"))

General form: (orelse instr1 instr2)

Run the first instruction. Then if it ``fails'', run the second instruction also; otherwise, stop after the first.

This instruction ``succeeds'' if and only if either instr1 ``succeeds'', or else instr2 ``succeeds''. If it ``fails'', then the failure is soft.