LOGIC

to set the default defun-mode to :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.