Major Section: BREAK-REWRITE
Examples: (unmonitor '(:rewrite assoc-of-app)) :unmonitor (:rewrite assoc-of-app) :unmonitor :allHere,General Forms: (unmonitor rune) (unmonitor :all)
rune
is a rune that is currently among those with break points
installed. This function removes the break.
Subtle point: Because you may want to unmonitor a ``rune'' that is
no longer a rune in the current ACL2 world, we don't actually check
this about rune. Instead, we simply check that rune is a consp
beginning with a keywordp
. That way, you'll know you've made a
mistake if you try to :unmonitor binary-append
instead of
:unmonitor (:definition binary-append)
, for example.