To disallow forced case-splits
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.
:in-theory (disable (:executable-counterpart force)) :in-theory (disable (force))
The following example shows how this works. First evaluate these forms.
(defstub f1 (x) t) (defstub f2 (x) t) (defaxiom ax (implies (case-split (f2 x)) (f1 x))) (thm (f1 x))
You will see the application of the rule,