Included Books
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc data-structures :parents (macro-libraries) :short "The @('books/data-structures') library" :long "<p>Also see @(see std). The @('books/data-structures') library is much older, much smaller, and less maintained than the @('std') library.</p>")
include-book
(include-book "alist-defthms")
include-book
(include-book "alist-defuns")
include-book
(include-book "alist-theory")
include-book
(include-book "array1")
include-book
(include-book "defalist")
include-book
(include-book "deflist")
include-book
(include-book "list-defthms")
include-book
(include-book "list-defuns")
include-book
(include-book "list-theory")
include-book
(include-book "no-duplicates")
include-book
(include-book "number-list-defthms")
include-book
(include-book "number-list-defuns")
include-book
(include-book "number-list-theory")
include-book
(include-book "portcullis")
include-book
(include-book "set-defthms")
include-book
(include-book "set-defuns")
include-book
(include-book "set-theory")
include-book
(include-book "structures")
include-book
(include-book "utilities")