Major Section: MISCELLANEOUS
General Form: ACL2 !>:disable-immediate-force-modepThis event causes ACL2 to attack forced hypotheses immediately instead of delaying them to the next forcing round. See immediate-force-modep. Or for more basic information, first see force for a discussion of forced case splits.
Disable-immediate-force-modep is a macro that disables the executable
counterpart of the function symbol immediate-force-modep
. When
you want to disable this mode in hints, use a form such as:
:in-theory (disable (:executable-counterpart immediate-force-modep))