local to any books and encapsulate events
in which it occurs; see add-include-book-dir for a discussion of this aspect
of both macros.
include-book's :dir argument
Major Section: SWITCHES-PARAMETERS-AND-MODES
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 is local to any books and encapsulate events
in which it occurs; see add-include-book-dir for a discussion of this aspect
of both macros.