other
(in-package "XDOC")
other
(include-book "base")
other
(include-book "tools/include-raw" :dir :system)
other
(set-state-ok t)
other
(defttag :xdoc)
all-xdoc-topicsfunction
(defun all-xdoc-topics (state) (declare (xargs :stobjs state :verify-guards t)) (prog2$ (er hard? 'all-xdoc-topics "all-xdoc-topics not yet defined.") (read-acl2-oracle state)))
other
(include-raw "defxdoc-raw-impl.lsp")