Included Books
other
(in-package "ACL2")
include-book
(include-book "collect")
*builtin-logic-defun-names-that-can-be-disabled*constant
(defconst *builtin-logic-defun-names-that-can-be-disabled* (set-difference-eq *builtin-logic-defun-names* '(ancestors-check oncep-tp too-many-ifs-pre-rewrite too-many-ifs-post-rewrite initialize-event-user finalize-event-user print-clause-id-okp canonical-pathname acl2x-expansion-alist magic-ev-fncall set-ld-history-entry-user-data mfc-ap-fn mfc-relieve-hyp-fn mfc-relieve-hyp-ttree mfc-rw+-fn mfc-rw+-ttree mfc-rw-fn mfc-rw-ttree mfc-ts-fn mfc-ts-ttree brkpt1-brr-data-entry brkpt2-brr-data-entry update-brr-data-1 update-brr-data-2 brr-near-missp)))
disable-all-builtin-logic-defunsmacro
(defmacro disable-all-builtin-logic-defuns nil `(in-theory (disable ,@*BUILTIN-LOGIC-DEFUN-NAMES-THAT-CAN-BE-DISABLED*)))
disable-most-builtin-logic-defunsmacro
(defmacro disable-most-builtin-logic-defuns nil `(in-theory (disable ,@(SET-DIFFERENCE-EQ *BUILTIN-LOGIC-DEFUN-NAMES-THAT-CAN-BE-DISABLED* '(= /= EQ EQL)))))
*builtin-rewrite-rules-for-defaults*constant
(defconst *builtin-rewrite-rules-for-defaults* '(default-car default-cdr default-numerator default-denominator default-realpart default-imagpart default-code-char default-char-code default-coerce-1 default-coerce-2 default-coerce-3 default-complex-1 default-complex-2 default-unary-minus default-unary-/ default-+-1 default-+-2 default-*-1 default-*-2 default-<-1 default-<-2 default-intern-in-package-of-symbol default-pkg-imports))
other
(assert-event (subsetp-eq *builtin-rewrite-rules-for-defaults* *builtin-rewrite-defaxiom/defthm-names*))
disable-builtin-rewrite-rules-for-defaultsmacro
(defmacro disable-builtin-rewrite-rules-for-defaults nil `(in-theory (disable ,@*BUILTIN-REWRITE-RULES-FOR-DEFAULTS*)))