Major Section: MISCELLANEOUS
defun is processed and no
supplied, the function
default-ruler-extenders is used to obtain the
current ruler-extenders; see ruler-extenders. To find the default
ruler-extenders of the current ACL2 world, type
(default-ruler-extenders (w state)).
While events that change the default ruler-extenders are permitted
encapsulate or the text of a book, their effects are
local in scope to the duration of the encapsulation or inclusion.
See default-defun-mode for an analogous discussion for defun-modes.