other
(in-package "ACL2S")
other
(include-book "acl2s/acl2s-size" :dir :system :ttags :all)
other
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil)
other
(include-book "acl2s/base-theory" :dir :system :ttags :all)
other
(include-book "acl2s/custom" :dir :system :ttags :all)
other
(include-book "acl2s/interface/top" :dir :system :ttags :all)
other
(include-book "acl2s/interface/acl2s-utils/top" :dir :system :ttags :all)
other
(acl2s-common-settings)
other
(acl2s-defaults :set verbosity-level 1)
other
(value-triple (time-tracker nil))
other
(set-inhibit-warnings! "Invariant-risk" "theory")
other
(set-in-theory-redundant-okp t)
other
(make-event (er-progn (let ((state (set-print-case :downcase state))) (mv nil nil state)) (set-print-gv-defaults :conjunct t :substitute t) (set-brr-evisc-tuple nil state) (value '(value-triple :invisible))) :expansion? (value-triple :invisible) :on-behalf-of :quiet! :save-event-data t)