Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: ACL2 p!>:logic ACL2 !>Typing the keyword
:logicsets the default defun-mode to
Functions defined in
:logic mode are logically defined.
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 equivalent to
(table acl2-defaults-table :defun-mode :logic),
and hence is
local to any books and
in which it occurs. See acl2-defaults-table.
Recall that the top-level form
:logic is equivalent to
see keyword-commands. Thus, to change the default defun-mode
:logic in a book, use
(logic), which is an embedded event
form, rather than
:logic, which is not a legal form for books.