/usr/share/acl2-6.3/books/xdoc/book-thms-example.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 11 12 | (IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(INCLUDE-BOOK "str/portcullis" :DIR :SYSTEM)
(INCLUDE-BOOK "oslib/portcullis" :DIR :SYSTEM)
(INCLUDE-BOOK "centaur/bridge/portcullis" :DIR :SYSTEM)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (LOCAL (ENCAPSULATE-THEN-NEW-INFO MY-NAME (DEFTHM FOO (EQUAL (CAR (CONS X Y)) X)) (DEFUN F1 (X Y) (<= X Y)) (DEFTHM BAR (< (ACL2-COUNT X) (ACL2-COUNT (CONS X Y)))) (DEFUN-SK EXISTS-X-F1 (Y) (EXISTS X (F1 X Y))) (ENCAPSULATE ((F (X) T) (H (X) T)) (LOCAL (DEFUN F (X) X)) (DEFUN G (X) (F X)) (LOCAL (DEFUN H (X) X)) (DEFTHM MY-THM (EQUAL (F X) (H (G X))))) (DEFCHOOSE MY-CH (X) (Y) (F1 X (CONS 0 Y))))) (LOCAL (VALUE-TRIPLE :ELIDED))))
(("/usr/share/acl2-6.3/books/centaur/bridge/portcullis.lisp" "centaur/bridge/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 661758845) ("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "oslib/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/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/xdoc/book-thms-example.lisp" "book-thms-example" "book-thms-example" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1970249283) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/centaur/bridge/portcullis.lisp" "centaur/bridge/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 661758845) ("/usr/share/acl2-6.3/books/oslib/portcullis.lisp" "oslib/portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197838065) ("/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))
1262379056
|