(table acl2-defaults-table :include-book-dir-alist ...)
and hence is local to any books and encapsulate events
in which it occurs. See acl2-defaults-table.
include-book's :dir argument
Major Section: EVENTS
Example Forms: (delete-include-book-dir :smith) ; Remove association of directory with :smith for include-book.whereGeneral Form: (delete-include-book-dir kwd)
kwd is a keywordp. The effect of this event is to modify the
meaning of the :dir keyword argument of include-book as indicated
by the examples above, namely by removing association of any directory with
the indicated keyword for purposes of the include-book :dir
argument. Normally one would instead use add-include-book-dir to
associate a new directory with that keyword; see add-include-book-dir.Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
This macro generates a call
(table acl2-defaults-table :include-book-dir-alist ...)
and hence is local to any books and encapsulate events
in which it occurs. See acl2-defaults-table.