defun'd functions
Major Section: MISCELLANEOUS
When a defun is processed and no :ruler-extenders xarg is
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
within an 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.
