ENABLE-IMMEDIATE-FORCE-MODEP

forced hypotheses are attacked immediately
Major Section:  MISCELLANEOUS

General Form:
ACL2 !>:enable-immediate-force-modep
This 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.

Enable-immediate-force-modep is a macro that enables the executable counterpart of the function symbol immediate-force-modep. When you want to enable this mode in hints, use a form such as:

:in-theory (enable (:executable-counterpart immediate-force-modep))