Included Books
other
(in-package "ACL2")
include-book
(include-book "number-list-defuns")
include-book
(include-book "number-list-defthms")
other
(deftheory number-list-theory (union-theories (theory 'number-list-defuns) (theory 'number-list-defthms)))