Included Books
other
(in-package "ACL2")
other
(deflabel beginning-of-apply-book)
include-book
(include-book "base")
other
(make-event (let ((world (w state))) `(deftheory apply-book-theory ',(SET-DIFFERENCE-EQUAL (CURRENT-THEORY :HERE) (CURRENT-THEORY 'BEGINNING-OF-APPLY-BOOK)))))