other
(in-package "ACL2S")
other
(deflabel pre-cgen)
other
(set-tau-auto-mode nil)
other
(include-book "top")
other
(set-tau-auto-mode t)
other
(in-theory (current-theory 'pre-cgen))
(in-package "ACL2S")
(deflabel pre-cgen)
(set-tau-auto-mode nil)
(include-book "top")
(set-tau-auto-mode t)
(in-theory (current-theory 'pre-cgen))