DISABLE-FORCING

to disallow forced case-splits 
Major Section:  MISCELLANEOUS


General Form:
ACL2 !>:disable-forcing   ; disallow forced case splits
See 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))