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