|
|
|---|
|
|
|
|---|
Functions whose definitions are "built in" to ACL2.
If you execute (IN-THEORY NIL), ACL2 prints a warning that the empty theory does not contain the :DEFINITION rules for certain functions whose definitions are built into ACL2 at various places. This theory contains the DEFUN-THEORY (see :DOC DEFUN-THEORY) of exactly those functions named in that message.