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