acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / hacking / hacker.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
:EXPANSION-ALIST
((4 RECORD-EXPANSION (MAKE-EVENT (IF (EARLIER-ACL2-VERSIONP "ACL2 Version 3.2" (@ ACL2-VERSION)) (VALUE (QUOTE (DEFMACRO PROGN!-WITH-BINDINGS (BINDINGS &REST RST) (CONS (QUOTE PROGN!) (CONS (QUOTE :STATE-GLOBAL-BINDINGS) (CONS BINDINGS RST)))))) (VALUE (QUOTE (DEFMACRO PROGN!-WITH-BINDINGS (BINDINGS &REST RST) (CONS (QUOTE PROGN!) (CONS (CONS (QUOTE STATE-GLOBAL-LET*) (CONS BINDINGS (CONS (CONS (QUOTE PROGN!) RST) (QUOTE NIL)))) (QUOTE NIL)))))))) (DEFMACRO PROGN!-WITH-BINDINGS (BINDINGS &REST RST) (CONS (QUOTE PROGN!) (CONS (QUOTE :STATE-GLOBAL-BINDINGS) (CONS BINDINGS RST))))) (24 RECORD-EXPANSION (MAKE-EVENT (IF (MEMBER-EQ (QUOTE PROGRAM-FNS-WITH-RAW-CODE) (GLOBAL-VAL (QUOTE UNTOUCHABLE-VARS) (W STATE))) (VALUE (QUOTE (DEFCONST ACL2-HACKER::*PROGRAM-ONLY-STATE-GLOBAL* (QUOTE PROGRAM-FNS-WITH-RAW-CODE)))) (VALUE (QUOTE (DEFCONST ACL2-HACKER::*PROGRAM-ONLY-STATE-GLOBAL* (QUOTE BUILT-IN-PROGRAM-MODE-FNS)))))) (DEFCONST ACL2-HACKER::*PROGRAM-ONLY-STATE-GLOBAL* (QUOTE PROGRAM-FNS-WITH-RAW-CODE))))
NIL
(("/usr/share/acl2-6.3/books/hacking/hacker.lisp" "hacker" "hacker" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 197252797) ("/usr/share/acl2-6.3/books/hacking/doc-section.lisp" "doc-section" "doc-section" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1293647265))
1403871894