acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / hacking / bridge.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "ACL2-HACKER" (APPEND (QUOTE (VALUE SET-W! ASSERT-EVENT MSG LD-EVISC-TUPLE CONNECTED-BOOK-DIRECTORY GUARD-CHECKING-ON INHIBIT-OUTPUT-LST PRINT-CLAUSE-IDS ACL2-RAW-MODE-P RAW-MODE-RESTORE-LST SAVED-OUTPUT-TOKEN-LST TAINTED-OKP IN-PACKAGE-FN DEFPKG-FN PE! TRANS! PSO PSO! VALUE-TRIPLE DEFAULT-EVISC-TUPLE TTAG HARD SOFT PROGN! UNTOUCHABLE-FNS UNTOUCHABLE-VARS LD-REDEFINITION-ACTION SET-LD-SKIP-PROOFSP SET-LD-REDEFINITION-ACTION SET-LD-PROMPT SET-LD-KEYWORD-ALIASES SET-LD-PRE-EVAL-FILTER SET-LD-ERROR-TRIPLES SET-LD-ERROR-ACTION SET-LD-QUERY-CONTROL-ALIST SET-CBD-FN SET-RAW-MODE SET-RAW-MODE-FN SET-TAINTED-OKP PUSH-UNTOUCHABLE-FN REMOVE-UNTOUCHABLE-FN SET-RAW-MODE-ON SET-RAW-MODE-OFF TEMP-TOUCHABLE-VARS TEMP-TOUCHABLE-FNS SET-TEMP-TOUCHABLE-VARS SET-TEMP-TOUCHABLE-FNS BUILT-IN-PROGRAM-MODE-FNS PROGRAM-FNS-WITH-RAW-CODE GLOBAL-VALUE CURRENT-ACL2-WORLD LD-LEVEL *WORMHOLEP* RAW-MODE-P MAX-ABSOLUTE-EVENT-NUMBER GETPROP ER-LET* *VALID-OUTPUT-NAMES* STATE-GLOBAL-LET* EXTENSION ABSOLUTE-TO-RELATIVE-COMMAND-NUMBER ACCESS-COMMAND-TUPLE-NUMBER GLOBAL-SET-LST COMMAND-NUMBER-BASELINE EVENT-NUMBER-BASELINE NEXT-ABSOLUTE-COMMAND-NUMBER ADD-COMMAND-LANDMARK NEXT-ABSOLUTE-EVENT-NUMBER ADD-EVENT-LANDMARK SCAN-TO-COMMAND CERTIFY-BOOK-FN F-GET-GLOBAL F-PUT-GLOBAL F-BOUNDP-GLOBAL CHECKPOINT-PROCESSORS GLOBAL-VAL ACL2-VERSION EARLIER-ACL2-VERSIONP)) (QUOTE (PROGN!-WITH-BINDINGS HACKER PROGN+TOUCHABLE PROGN=TOUCHABLE PROGN!+TOUCHABLE PROGN!=TOUCHABLE WITH-TOUCHABLE PROGN+REDEF WITH-REDEF-ALLOWED IN-RAW-MODE WITH-RAW-MODE ASSERT-PROGRAM-MODE ENSURE-PROGRAM-ONLY-FLAG ENSURE-PROGRAM-ONLY HAS-SPECIAL-RAW-DEFINITION ENSURE-SPECIAL-RAW-DEFINITION-FLAG ASSERT-NO-SPECIAL-RAW-DEFINITION RECONSTRUCT-DECLARE-LST MODIFY-RAW-DEFUN-PERMANENT PROGN+ALL-TTAGS-ALLOWED DEFLABELS TTAG-SKIP-PROOFS PROGN+TTAG-SKIP-PROOFS)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)))
:END-PORTCULLIS-CMDS
NIL
(("/usr/share/acl2-6.3/books/hacking/bridge.lisp" "bridge" "bridge" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 690072471) ("/usr/share/acl2-6.3/books/hacking/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1293647265))
329447960