/usr/share/acl2-6.3/books/xdoc/defsection-tests.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 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 | (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
((2 RECORD-EXPANSION (DEFXDOC XDOC::TEST :SHORT "Test of defsection") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . XDOC::TEST) (:BASE-PKG . XDOC::ACL2-PKG-WITNESS) (:PARENTS) (:SHORT . "Test of defsection") (:LONG) (:FROM . "[books]/xdoc/defsection-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC XDOC::TEST)))))) (3 RECORD-EXPANSION (DEFSECTION XDOC::FOO1 :PARENTS (XDOC::TEST) :AUTODOC NIL (DEFUN XDOC::FOO1 (XDOC::X) XDOC::X)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (RECORD-EXPANSION (DEFXDOC XDOC::FOO1 :PARENTS (XDOC::TEST) :SHORT NIL :LONG NIL) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . XDOC::FOO1) (:BASE-PKG . XDOC::ACL2-PKG-WITNESS) (:PARENTS XDOC::TEST) (:SHORT) (:LONG) (:FROM . "[books]/xdoc/defsection-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC XDOC::FOO1)))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN XDOC::FOO1 (XDOC::X) XDOC::X)))))) (4 RECORD-EXPANSION (DEFSECTION XDOC::FOO2 :PARENTS (XDOC::TEST) (DEFUN XDOC::FOO2 (XDOC::X) XDOC::X)) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO2)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUN XDOC::FOO2 (XDOC::X) XDOC::X))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE XDOC::FOO2)) (XDOC::PARENTS (QUOTE (XDOC::TEST))) (XDOC::SHORT (QUOTE NIL)) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO2))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . XDOC::FOO2) (:BASE-PKG . XDOC::ACL2-PKG-WITNESS) (:PARENTS XDOC::TEST) (:SHORT) (:LONG . "
<h3>Definitions and Theorems</h3>@(def |XDOC|::|FOO2|)") (:FROM . "[books]/xdoc/defsection-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC XDOC::FOO2)))))) (VALUE-TRIPLE (QUOTE XDOC::FOO2))))) (5 RECORD-EXPANSION (DEFSECTION XDOC::FOO3 :PARENTS (XDOC::TEST) :SHORT "Section for foo3" :LONG "<p>Foo3 is wonderful.</p>" (DEFUND XDOC::FOO3 (XDOC::X) (+ 1 XDOC::X)) (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::NATP-OF-FOO3 (IMPLIES (NATP XDOC::X) (NATP (XDOC::FOO3 XDOC::X)))) (LOCAL (DEFTHM XDOC::FOO3-LEMMA (IMPLIES (EQUAL XDOC::X 3) (EQUAL (XDOC::FOO3 XDOC::X) 4)))) (DEFMACRO XDOC::FOO3-ALIAS (XDOC::X) (CONS (QUOTE XDOC::FOO3) (CONS XDOC::X (QUOTE NIL)))) (DEFSECTION XDOC::BAR :PARENTS (XDOC::TEST) :SHORT "Section for bar" :LONG "<p>Bar is wonderful.</p>" (DEFUND XDOC::BAR (XDOC::X) (+ 2 XDOC::X)))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO3)) (RECORD-EXPANSION (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND XDOC::FOO3 (XDOC::X) (+ 1 XDOC::X)) (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::NATP-OF-FOO3 (IMPLIES (NATP XDOC::X) (NATP (XDOC::FOO3 XDOC::X)))) (LOCAL (DEFTHM XDOC::FOO3-LEMMA (IMPLIES (EQUAL XDOC::X 3) (EQUAL (XDOC::FOO3 XDOC::X) 4)))) (DEFMACRO XDOC::FOO3-ALIAS (XDOC::X) (CONS (QUOTE XDOC::FOO3) (CONS XDOC::X (QUOTE NIL)))) (DEFSECTION XDOC::BAR :PARENTS (XDOC::TEST) :SHORT "Section for bar" :LONG "<p>Bar is wonderful.</p>" (DEFUND XDOC::BAR (XDOC::X) (+ 2 XDOC::X))))) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND XDOC::FOO3 (XDOC::X) (+ 1 XDOC::X)) (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::NATP-OF-FOO3 (IMPLIES (NATP XDOC::X) (NATP (XDOC::FOO3 XDOC::X)))) (LOCAL (DEFTHM XDOC::FOO3-LEMMA (IMPLIES (EQUAL XDOC::X 3) (EQUAL (XDOC::FOO3 XDOC::X) 4)))) (DEFMACRO XDOC::FOO3-ALIAS (XDOC::X) (CONS (QUOTE XDOC::FOO3) (CONS XDOC::X (QUOTE NIL)))) (RECORD-EXPANSION (DEFSECTION XDOC::BAR :PARENTS (XDOC::TEST) :SHORT "Section for bar" :LONG "<p>Bar is wonderful.</p>" (DEFUND XDOC::BAR (XDOC::X) (+ 2 XDOC::X))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE XDOC::BAR)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (DEFUND XDOC::BAR (XDOC::X) (+ 2 XDOC::X)))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE XDOC::BAR)) (XDOC::PARENTS (QUOTE (XDOC::TEST))) (XDOC::SHORT (QUOTE "Section for bar")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE XDOC::BAR))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Bar is wonderful.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . XDOC::BAR) (:BASE-PKG . XDOC::ACL2-PKG-WITNESS) (:PARENTS XDOC::TEST) (:SHORT . "Section for bar") (:LONG . "<p>Bar is wonderful.</p>
<h3>Definitions and Theorems</h3>@(def |XDOC|::|BAR|)") (:FROM . "[books]/xdoc/defsection-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC XDOC::BAR)))))) (VALUE-TRIPLE (QUOTE XDOC::BAR)))))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE XDOC::FOO3)) (XDOC::PARENTS (QUOTE (XDOC::TEST))) (XDOC::SHORT (QUOTE "Section for foo3")) (XDOC::EXTENSION (QUOTE NIL)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO3))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<p>Foo3 is wonderful.</p>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . XDOC::FOO3) (:BASE-PKG . XDOC::ACL2-PKG-WITNESS) (:PARENTS XDOC::TEST) (:SHORT . "Section for foo3") (:LONG . "<p>Foo3 is wonderful.</p>
<h3>Definitions and Theorems</h3>@(def |XDOC|::|FOO3|)
@(def |XDOC|::|NATP-OF-FOO3|)
@(def |XDOC|::|BAR|)") (:FROM . "[books]/xdoc/defsection-tests.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC XDOC::FOO3)))))) (VALUE-TRIPLE (QUOTE XDOC::FOO3))))) (6 RECORD-EXPANSION (DEFSECTION XDOC::FOO3-ADVANCED :EXTENSION XDOC::FOO3 (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::POSP-OF-FOO3 (IMPLIES (NATP XDOC::X) (POSP (XDOC::FOO3 XDOC::X)))) (DEFTHM XDOC::ODDP-OF-FOO3 (IMPLIES (EVENP XDOC::X) (ODDP (XDOC::FOO3 XDOC::X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO3-ADVANCED)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::POSP-OF-FOO3 (IMPLIES (NATP XDOC::X) (POSP (XDOC::FOO3 XDOC::X)))) (DEFTHM XDOC::ODDP-OF-FOO3 (IMPLIES (EVENP XDOC::X) (ODDP (XDOC::FOO3 XDOC::X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE XDOC::FOO3-ADVANCED)) (XDOC::PARENTS (QUOTE NIL)) (XDOC::SHORT (QUOTE NIL)) (XDOC::EXTENSION (QUOTE XDOC::FOO3)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO3-ADVANCED))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE XDOC::FOO3) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING: Ignoring attempt to extend topic ~x0, ~
because no such topic is currently defined.~%" (QUOTE XDOC::FOO3)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) XDOC::OLD-LONG "
@(def |XDOC|::|POSP-OF-FOO3|)
@(def |XDOC|::|ODDP-OF-FOO3|)")) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))) (VALUE-TRIPLE (QUOTE XDOC::FOO3-ADVANCED))))) (7 RECORD-EXPANSION (DEFSECTION XDOC::FOO3-ADVANCED-MORE :EXTENSION XDOC::FOO3 :LONG "<h3>Even more theorems!</h3>" (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::INTEGERP-OF-FOO3 (IMPLIES (INTEGERP XDOC::X) (INTEGERP (XDOC::FOO3 XDOC::X))))) (WITH-OUTPUT :STACK :PUSH :OFF :ALL :ON ERROR (PROGN (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO3-ADVANCED-MORE)) (WITH-OUTPUT :STACK :POP (ENCAPSULATE NIL (VALUE-TRIPLE :INVISIBLE) (LOCAL (IN-THEORY (ENABLE XDOC::FOO3))) (DEFTHM XDOC::INTEGERP-OF-FOO3 (IMPLIES (INTEGERP XDOC::X) (INTEGERP (XDOC::FOO3 XDOC::X)))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((XDOC::NAME (QUOTE XDOC::FOO3-ADVANCED-MORE)) (XDOC::PARENTS (QUOTE NIL)) (XDOC::SHORT (QUOTE NIL)) (XDOC::EXTENSION (QUOTE XDOC::FOO3)) (XDOC::WRLD (W STATE)) (XDOC::TRIPS (REVERSED-WORLD-SINCE-EVENT XDOC::WRLD (QUOTE (TABLE INTRO-TABLE :MARK (QUOTE XDOC::FOO3-ADVANCED-MORE))) NIL)) (XDOC::INFO (REVERSE (NEW-FORMULA-INFO XDOC::TRIPS XDOC::WRLD NIL))) (XDOC::AUTODOC (XDOC::FORMULA-INFO-TO-DEFS (NOT XDOC::EXTENSION) XDOC::INFO)) (XDOC::LONG (CONCATENATE (QUOTE STRING) (QUOTE "<h3>Even more theorems!</h3>") (COERCE (LIST #\Newline #\Newline) (QUOTE STRING)) XDOC::AUTODOC))) (IF XDOC::EXTENSION (CONS (QUOTE XDOC-EXTEND) (CONS XDOC::EXTENSION (CONS XDOC::LONG (QUOTE NIL)))) (CONS (QUOTE DEFXDOC) (CONS XDOC::NAME (CONS (QUOTE :PARENTS) (CONS XDOC::PARENTS (CONS (QUOTE :SHORT) (CONS XDOC::SHORT (CONS (QUOTE :LONG) (CONS XDOC::LONG (QUOTE NIL)))))))))))) (TABLE XDOC (QUOTE DOC) (LET* ((XDOC::ALL-TOPICS (XDOC::GET-XDOC-TABLE WORLD)) (XDOC::OLD-TOPIC (XDOC::FIND-TOPIC (QUOTE XDOC::FOO3) XDOC::ALL-TOPICS))) (COND ((NOT XDOC::OLD-TOPIC) (PROG2$ (CW "XDOC WARNING: Ignoring attempt to extend topic ~x0, ~
because no such topic is currently defined.~%" (QUOTE XDOC::FOO3)) XDOC::ALL-TOPICS)) (T (LET* ((XDOC::OTHER-TOPICS (REMOVE-EQUAL XDOC::OLD-TOPIC XDOC::ALL-TOPICS)) (XDOC::OLD-LONG (CDR (ASSOC :LONG XDOC::OLD-TOPIC))) (XDOC::NEW-LONG (CONCATENATE (QUOTE STRING) XDOC::OLD-LONG "<h3>Even more theorems!</h3>
@(def |XDOC|::|INTEGERP-OF-FOO3|)")) (XDOC::NEW-TOPIC (ACONS :LONG XDOC::NEW-LONG (DELETE-ASSOC :LONG XDOC::OLD-TOPIC)))) (CONS XDOC::NEW-TOPIC XDOC::OTHER-TOPICS))))))) (VALUE-TRIPLE (QUOTE XDOC::FOO3-ADVANCED-MORE))))))
(("/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/defsection-tests.lisp" "defsection-tests" "defsection-tests" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 857457793) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/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/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573) ("/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))
1216479424
|