To allow forced case splits
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 an example showing how to turn off forced case splits.
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))