To set the default defun-mode to
Example: ACL2 !>:program ACL2 p!>
Typing the keyword
Functions defined in
Calls of the following macros are ignored (skipped) when in
local verify-guards verify-termination defaxiom defthm deftheory in-theory in-arithmetic-theory regenerate-tau-database theory-invariant defchoose
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
See defun-mode for a discussion of the defun-modes available
and what their effects on the logic are. See default-defun-mode for a
discussion of how the default defun-mode is used. This event is
Recall that the top-level form
See program-wrapper for how to use program-mode functions to avoid expensive guard checks.