Included Books
other
(in-package "ACL2")
include-book
(include-book "included-books")
include-book
(include-book "std/testing/assert-bang" :dir :system)
other
(assert! (string-listp (included-books (w state))))
other
(assert! (no-duplicatesp-equal (included-books (w state))))