ENABLE-FORCING

to allow forced case splits 
Major Section:  MISCELLANEOUS


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

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

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