ENABLE-FORCING

to allow forced splits 
Major Section:  MISCELLANEOUS


General Form:
ACL2 !>:enable-forcing    ; allowed forced case splits
See force and see case-split for a discussion of forced case splits, which are turned back on by this command. (See disable-forcing for how to turn them off.)

Enable-forcing is actually a macro that enables the executable counterpart of the function symbol force; see force. When you want to use hints to turn on forced case splits, use a form such as one of the following (these are equivalent). 

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