DISABLE-FORCING

to disallow forced case splits 
Major Section:  MISCELLANEOUS


General Form:
ACL2 !>:disable-forcing   ; disallow forced case splits
See force for a discussion of forced case splits.

Disable-forcing is a macro that disables the executable counterpart of the function symbol force; see force. When you want to disable forcing in hints, use a form such as: 

:in-theory (disable (:executable-counterpart force))