Major Section: SWITCHES-PARAMETERS-AND-MODES
Example Forms: (delete-include-book-dir :smith) ; Remove association of directory with :smith for include-book. General Form: (delete-include-book-dir kwd)where
keywordp. The effect of this event is to modify the meaning of the
:dirkeyword argument of
ldas indicated by the examples above, namely by removing association of any directory with the indicated keyword for purposes of the
:dirargument. Normally one would instead use
add-include-book-dirto 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
in which it occurs; see add-include-book-dir for a discussion of this aspect
of both macros.