Major Section: MISCELLANEOUS
General Form: ACL2 !>:disable-forcing ; disallow forced case splitsSee force and see case-split for a discussion of forced case splits, which are inhibited by this command.
Disable-forcing is actually a macro that disables the executable
counterpart of the function symbol
force; see force. When you want to
use hints to turn off forced case splits, use a form such as one of the
following (these are equivalent).
:in-theory (disable (:executable-counterpart force)) :in-theory (disable (force))