/usr/share/acl2-6.3/books/cutil/maybe-defthm.cert is in acl2-books-certs 6.3-5.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "portcullis")
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((6 RECORD-EXPANSION (LOCAL (PROGN (INCLUDE-BOOK "misc/assert" :DIR :SYSTEM) (CUTIL::MAYBE-DEFTHM-AS-REWRITE CUTIL::FOO (EQUAL (CAR (CONS CUTIL::X CUTIL::Y)) CUTIL::X)) (CUTIL::MAYBE-DEFTHM-AS-REWRITE CUTIL::BAR (EQUAL (NOT (QUOTE NIL)) (QUOTE T))) (CUTIL::MAYBE-DEFTHM-AS-REWRITE CUTIL::BAZ (EQUAL (STRINGP (QUOTE NIL)) (QUOTE NIL))) (ASSERT! (CUTIL::IS-THEOREM-P (QUOTE CUTIL::FOO) (W STATE))) (ASSERT! (NOT (CUTIL::IS-THEOREM-P (QUOTE CUTIL::BAR) (W STATE)))) (ASSERT! (NOT (CUTIL::IS-THEOREM-P (QUOTE CUTIL::BAZ) (W STATE)))) (ASSERT! (LET ((ENS (ENS STATE))) (ACTIVE-RUNEP (QUOTE (:REWRITE CUTIL::FOO))))) (ASSERT! (LET ((ENS (ENS STATE))) (NOT (ACTIVE-RUNEP (QUOTE (:REWRITE CUTIL::BAR)))))) (CUTIL::ENABLE-IF-THEOREM CUTIL::FOO) (ASSERT! (LET ((ENS (ENS STATE))) (ACTIVE-RUNEP (QUOTE (:REWRITE CUTIL::FOO))))) (CUTIL::DISABLE-IF-THEOREM CUTIL::FOO) (ASSERT! (LET ((ENS (ENS STATE))) (NOT (ACTIVE-RUNEP (QUOTE (:REWRITE CUTIL::FOO)))))) (CUTIL::ENABLE-IF-THEOREM CUTIL::FOO) (ASSERT! (LET ((ENS (ENS STATE))) (ACTIVE-RUNEP (QUOTE (:REWRITE CUTIL::FOO))))))) (LOCAL (VALUE-TRIPLE :ELIDED))))
(("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
(("/usr/share/acl2-6.3/books/cutil/maybe-defthm.lisp" "maybe-defthm" "maybe-defthm" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 169275099) (LOCAL ("/usr/share/acl2-6.3/books/misc/assert.lisp" "misc/assert" "assert" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1184956729)) (LOCAL ("/usr/share/acl2-6.3/books/misc/eval.lisp" "eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718)) ("/usr/share/acl2-6.3/books/tools/bstar.lisp" "tools/bstar" "bstar" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1482974359) ("/usr/share/acl2-6.3/books/tools/pack.lisp" "pack" "pack" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1797170439) ("/usr/share/acl2-6.3/books/cutil/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1188104018) ("/usr/share/acl2-6.3/books/std/osets/portcullis.lisp" "std/osets/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1689687557) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "xdoc/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/usr/share/acl2-6.3/books/str/portcullis.lisp" "str/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2077071243))
1048543741
|