Included Books
other
(in-package "ACL2")
include-book
(include-book "tools/include-raw" :dir :system)
other
(set-ignore-ok t)
other
(make-event (er-progn (assign command-result nil) (value '(value-triple (@ command-result)))) :check-expansion t)
other
(defttag :acl2s-interface)
other
(include-raw "acl2s-interface.lsp")
other
(include-raw "acl2s-interface-utils.lsp")
include-book
(include-book "doc")