Searched refs:WRITE (Results 1 - 23 of 23) sorted by relevance

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DFile.h24 enum FileMode { READ, WRITE }; enumerator in enum:FileMode
95 assert(mode == WRITE);
103 if (mode == WRITE) setMode(READ);
107 if (mode == READ) setMode(WRITE);
120 assert(mode == WRITE);
H A DFile.C39 mode = has_r ? READ : WRITE;
53 if (mode == WRITE)
63 if (mode == WRITE){
77 if (mode == WRITE)
H A DProof.C97 fp.setMode(WRITE);
148 fp.setMode(WRITE);
360 fp.setMode(WRITE);
414 fp.setMode(WRITE);
/seL4-l4v-master/HOL4/src/monad/more_monads/
H A Dstate_monadLib.sml58 `WRITE f s`,
H A Dstate_transformerSyntax.sml63 val (write_tm, mk_write, dest_write, is_write) = s1 "WRITE"
H A Dstate_transformerScript.sml61 (WRITE : ('state -> 'state) -> (unit, 'state) M) f = \s. ((), f s)`;
H A DerrorStateMonadScript.sml53 (WRITE : ('state -> 'state) -> (unit, 'state) M) f = \s. SOME ((), f s)`;
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DIRSyntax.sml346 datatype ACCESS = READ | WRITE | PUSH | POP
361 | ch_mode (m,UNKNOWN) WRITE = (m, OUTPUT)
362 | ch_mode (m,OUTPUT) WRITE = (m,OUTPUT)
365 | ch_mode (m,INSTACK) WRITE = (m,OUTPUT)
377 List.map (fn exp => update_mode exp WRITE) dst1
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DIRSyntax.sml338 datatype ACCESS = READ | WRITE | PUSH | POP
353 | ch_mode (m,UNKNOWN) WRITE = (m, OUTPUT)
354 | ch_mode (m,OUTPUT) WRITE = (m,OUTPUT)
357 | ch_mode (m,INSTACK) WRITE = (m,OUTPUT)
369 List.map (fn exp => update_mode exp WRITE) dst1
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DIRSyntax.sml338 datatype ACCESS = READ | WRITE | PUSH | POP
353 | ch_mode (m,UNKNOWN) WRITE = (m, OUTPUT)
354 | ch_mode (m,OUTPUT) WRITE = (m,OUTPUT)
357 | ch_mode (m,INSTACK) WRITE = (m,OUTPUT)
369 List.map (fn exp => update_mode exp WRITE) dst1
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dkpa-v2-9-3.ml748 ("WRITE-BYTE$", "ACL2-USER", "ACL2"),
1124 ("FILE-WRITE-DATE", "ACL2-USER", "COMMON-LISP"),
1724 ("WRITE", "ACL2-USER", "COMMON-LISP"),
1726 ("WRITE-BYTE", "ACL2-USER", "COMMON-LISP"),
1728 ("WRITE-CHAR", "ACL2-USER", "COMMON-LISP"),
1730 ("WRITE-LINE", "ACL2-USER", "COMMON-LISP"),
1732 ("WRITE-SEQUENCE", "ACL2-USER", "COMMON-LISP"),
1734 ("WRITE-STRING", "ACL2-USER", "COMMON-LISP"),
1736 ("WRITE-TO-STRING", "ACL2-USER", "COMMON-LISP"),
2102 ("FILE-WRITE
[all...]
H A Dhol_defaxioms_proofsScript.sml2281 csym "FILE-WRITE-DATE";
2595 csym "UNWIND-PROTECT"; csym "WRITE";
2597 csym "WRITE-BYTE";
2599 csym "WRITE-CHAR";
2601 csym "WRITE-LINE";
2603 csym "WRITE-SEQUENCE"; csym "UPPER-CASE-P";
2604 csym "WRITE-STRING"; csym "USE-PACKAGE";
2605 csym "WRITE-TO-STRING"; csym "USE-VALUE";
2878 csym "FILE-WRITE-DATE";
3192 csym "UNWIND-PROTECT"; csym "WRITE";
[all...]
H A Dacl2_packageScript.sml859 ("WRITE-BYTE$", "ACL2-USER", "ACL2"),
1235 ("FILE-WRITE-DATE", "ACL2-USER", "COMMON-LISP"),
1835 ("WRITE", "ACL2-USER", "COMMON-LISP"),
1837 ("WRITE-BYTE", "ACL2-USER", "COMMON-LISP"),
1839 ("WRITE-CHAR", "ACL2-USER", "COMMON-LISP"),
1841 ("WRITE-LINE", "ACL2-USER", "COMMON-LISP"),
1843 ("WRITE-SEQUENCE", "ACL2-USER", "COMMON-LISP"),
1845 ("WRITE-STRING", "ACL2-USER", "COMMON-LISP"),
1847 ("WRITE-TO-STRING", "ACL2-USER", "COMMON-LISP"),
2213 ("FILE-WRITE
[all...]
H A Dhol_defaxiomsScript.sml3687 [oracles: DEFUN ACL2::WRITE-BYTE$, DISK_THM] [axioms: ] []
H A Ddefaxioms.lisp.trans.ml6998 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "WRITE-BYTE$") (
10661 mkpair (mksym "COMMON-LISP" "FILE-WRITE-DATE") (mkpair (mksym "COMMON-LISP"
11037 mkpair (mksym "COMMON-LISP" "WRITE") (mkpair (mksym "COMMON-LISP"
11039 "WRITE-BYTE") (mkpair (mksym "COMMON-LISP"
11041 "WRITE-CHAR") (mkpair (mksym "COMMON-LISP" "UPGRADED-ARRAY-ELEMENT-TYPE") (
11042 mkpair (mksym "COMMON-LISP" "WRITE-LINE") (mkpair (mksym "COMMON-LISP"
11043 "UPGRADED-COMPLEX-PART-TYPE") (mkpair (mksym "COMMON-LISP" "WRITE-SEQUENCE") (
11045 "WRITE-STRING") (mkpair (mksym "COMMON-LISP" "USE-PACKAGE") (mkpair (mksym
11046 "COMMON-LISP" "WRITE-TO-STRING") (mkpair (mksym "COMMON-LISP" "USE-VALUE") (
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A DPKGS.sml403 ("FILE-WRITE-DATE" , "ACL2" , "COMMON-LISP"),
1003 ("WRITE" , "ACL2" , "COMMON-LISP"),
1005 ("WRITE-BYTE" , "ACL2" , "COMMON-LISP"),
1007 ("WRITE-CHAR" , "ACL2" , "COMMON-LISP"),
1009 ("WRITE-LINE" , "ACL2" , "COMMON-LISP"),
1011 ("WRITE-SEQUENCE" , "ACL2" , "COMMON-LISP"),
1013 ("WRITE-STRING" , "ACL2" , "COMMON-LISP"),
1015 ("WRITE-TO-STRING" , "ACL2" , "COMMON-LISP"),
1687 ("FILE-WRITE-DATE" , "ACL2-USER" , "COMMON-LISP"),
2842 ("WRITE" , "ACL
[all...]
H A Daxioms.ml3173 mkpair (mksym "COMMON-LISP" "FILE-WRITE-DATE") (mkpair (mksym "COMMON-LISP"
3549 mkpair (mksym "COMMON-LISP" "WRITE") (mkpair (mksym "COMMON-LISP"
3551 "WRITE-BYTE") (mkpair (mksym "COMMON-LISP"
3553 "WRITE-CHAR") (mkpair (mksym "COMMON-LISP" "UPGRADED-ARRAY-ELEMENT-TYPE") (
3554 mkpair (mksym "COMMON-LISP" "WRITE-LINE") (mkpair (mksym "COMMON-LISP"
3555 "UPGRADED-COMPLEX-PART-TYPE") (mkpair (mksym "COMMON-LISP" "WRITE-SEQUENCE") (
3557 "WRITE-STRING") (mkpair (mksym "COMMON-LISP" "USE-PACKAGE") (mkpair (mksym
3558 "COMMON-LISP" "WRITE-TO-STRING") (mkpair (mksym "COMMON-LISP" "USE-VALUE") (
9828 mkpair (mksym "ACL2" "WRITE-BYTE$") (mkpair (mksym "ACL2" "SHRINK-T-STACK") (
10055 mksym "ACL2" "LD-FN") (mkpair (mksym "ACL2" "WRITE
[all...]
H A Dhol_defaxiomsScript.sml3729 [oracles: DEFUN ACL2::WRITE-BYTE$, DISK_THM] [axioms: ] []
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/
H A DPKGS.sml362 ("FILE-WRITE-DATE" , "ACL2" , "COMMON-LISP"),
962 ("WRITE" , "ACL2" , "COMMON-LISP"),
964 ("WRITE-BYTE" , "ACL2" , "COMMON-LISP"),
966 ("WRITE-CHAR" , "ACL2" , "COMMON-LISP"),
968 ("WRITE-LINE" , "ACL2" , "COMMON-LISP"),
970 ("WRITE-SEQUENCE" , "ACL2" , "COMMON-LISP"),
972 ("WRITE-STRING" , "ACL2" , "COMMON-LISP"),
974 ("WRITE-TO-STRING" , "ACL2" , "COMMON-LISP"),
1646 ("FILE-WRITE-DATE" , "ACL2-USER" , "COMMON-LISP"),
2801 ("WRITE" , "ACL
[all...]
H A DPKGS.lsp2 (("ACL2-CRG" & &ALLOW-OTHER-KEYS &AUX &BODY &ENVIRONMENT &KEY &OPTIONAL &REST &WHOLE * ** *** *ACL2-EXPORTS* *BREAK-ON-SIGNALS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *COMPILE-FILE-PATHNAME* *COMPILE-FILE-TRUENAME* *COMPILE-PRINT* *COMPILE-VERBOSE* *DEBUG-IO* *DEBUGGER-HOOK* *DEFAULT-PATHNAME-DEFAULTS* *ERROR-OUTPUT* *FEATURES* *GENSYM-COUNTER* *LOAD-PATHNAME* *LOAD-PRINT* *LOAD-TRUENAME* *LOAD-VERBOSE* *MACROEXPAND-HOOK* *MAIN-LISP-PACKAGE-NAME* *MODULES* *PACKAGE* *PRINT-ARRAY* *PRINT-BASE* *PRINT-CASE* *PRINT-CIRCLE* *PRINT-ESCAPE* *PRINT-GENSYM* *PRINT-LENGTH* *PRINT-LEVEL* *PRINT-LINES* *PRINT-MISER-WIDTH* *PRINT-PPRINT-DISPATCH* *PRINT-PRETTY* *PRINT-RADIX* *PRINT-READABLY* *PRINT-RIGHT-MARGIN* *QUERY-IO* *RANDOM-STATE* *READ-BASE* *READ-DEFAULT-FLOAT-FORMAT* *READ-EVAL* *READ-SUPPRESS* *READTABLE* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-INPUT* *STANDARD-OI* *STANDARD-OUTPUT* *TERMINAL-IO* *TRACE-OUTPUT* + ++ +++ - / // /// /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACOS ACOSH ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-METHOD ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ADJOIN ADJUST-ARRAY ADJUSTABLE-ARRAY-P ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALLOCATE-INSTANCE ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP ALPHANUMERICP AND AND-MACRO APPEND APPLY APROPOS APROPOS-LIST AREF AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARITHMETIC-ERROR ARITHMETIC-ERROR-OPERANDS ARITHMETIC-ERROR-OPERATION ARRAY ARRAY-DIMENSION ARRAY-DIMENSION-LIMIT ARRAY-DIMENSIONS ARRAY-DISPLACEMENT ARRAY-ELEMENT-TYPE ARRAY-HAS-FILL-POINTER-P ARRAY-IN-BOUNDS-P ARRAY-RANK ARRAY-RANK-LIMIT ARRAY-ROW-MAJOR-INDEX ARRAY-TOTAL-SIZE ARRAY-TOTAL-SIZE-LIMIT ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ARRAYP ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASIN ASINH ASSERT ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-IF ASSOC-IF-NOT ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2 ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+ ASSUME ATAN ATANH ATOM ATOM-LISTP ATOM-LISTP-FORWARD-TO-TRUE-LISTP BASE-CHAR BASE-STRING BIG-CLOCK-ENTRY BIG-CLOCK-NEGATIVE-P BIGNUM BINARY-* BINARY-+ BINARY-APPEND BIND-FREE BINOP-TABLE BIT BIT-AND BIT-ANDC1 BIT-ANDC2 BIT-EQV BIT-IOR BIT-NAND BIT-NOR BIT-NOT BIT-ORC1 BIT-ORC2 BIT-VECTOR BIT-VECTOR-P BIT-XOR BLOCK BOOLE BOOLE-1 BOOLE-2 BOOLE-AND BOOLE-ANDC1 BOOLE-ANDC2 BOOLE-C1 BOOLE-C2 BOOLE-CLR BOOLE-EQV BOOLE-IOR BOOLE-NAND BOOLE-NOR BOOLE-ORC1 BOOLE-ORC2 BOOLE-SET BOOLE-XOR BOOLEAN BOOLEAN-LISTP BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP BOOLEANP BOOLEANP-CHARACTERP BOOLEANP-COMPOUND-RECOGNIZER BOTH-CASE-P BOUNDED-INTEGER-ALISTP BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP BOUNDED-INTEGER-ALISTP2 BOUNDP BOUNDP-GLOBAL BOUNDP-GLOBAL1 BREAK BROADCAST-STREAM BROADCAST-STREAM-STREAMS BRR BRR@ BUILD-STATE1 BUILT-IN-CLASS BUTLAST BYTE BYTE-POSITION BYTE-SIZE CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CALL-ARGUMENTS-LIMIT CALL-METHOD CALL-NEXT-METHOD CAR CAR-CDR-ELIM CAR-CONS CASE CASE-LIST CASE-LIST-CHECK CASE-MATCH CASE-SPLIT CASE-TEST CATCH CBD CCASE CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR CDR CDR-CONS CDRN CEILING CELL-ERROR CELL-ERROR-NAME CERROR CERTIFY-BOOK CERTIFY-BOOK! CHANGE-CLASS CHAR CHAR-CODE CHAR-CODE-CODE-CHAR-IS-IDENTITY CHAR-CODE-LIMIT CHAR-CODE-LINEAR CHAR-DOWNCASE CHAR-EQUAL CHAR-GREATERP CHAR-INT CHAR-LESSP CHAR-NAME CHAR-NOT-EQUAL CHAR-NOT-GREATERP CHAR-NOT-LESSP CHAR-UPCASE CHAR/= CHAR< CHAR<= CHAR= CHAR> CHAR>= CHARACTER CHARACTER-LISTP CHARACTER-LISTP-APPEND CHARACTER-LISTP-COERCE CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP CHARACTER-LISTP-REMOVE-DUPLICATES-EQL CHARACTER-LISTP-REVAPPEND CHARACTER-LISTP-STRING-DOWNCASE-1 CHARACTER-LISTP-STRING-UPCASE1-1 CHARACTERP CHARACTERP-CHAR-DOWNCASE CHARACTERP-CHAR-UPCASE CHARACTERP-NTH CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-TAB CHECK-TYPE CHECK-VARS-NOT-FREE CHECKPOINT-FORCED-GOALS CIS CLASS CLASS-NAME CLASS-OF CLAUSE CLEAR-HASH-TABLES CLEAR-INPUT CLEAR-MEMOIZE-TABLE CLEAR-MEMOIZE-TABLES CLEAR-OUTPUT CLOSE CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL CLOSE-TRACE-FILE CLOSURE CLRHASH CODE-CHAR CODE-CHAR-CHAR-CODE-IS-IDENTITY CODE-CHAR-TYPE COERCE COERCE-INVERSE-1 COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE COERCE-STATE-TO-OBJECT COMMUTATIVITY-OF-* COMMUTATIVITY-OF-+ COMP COMPILATION-SPEED COMPILE COMPILE-FILE COMPILE-FILE-PATHNAME COMPILED-FUNCTION COMPILED-FUNCTION-P COMPILER-MACRO COMPILER-MACRO-FUNCTION COMPLEMENT COMPLETION-OF-* COMPLETION-OF-+ COMPLETION-OF-< COMPLETION-OF-CAR COMPLETION-OF-CDR COMPLETION-OF-CHAR-CODE COMPLETION-OF-CODE-CHAR COMPLETION-OF-COERCE COMPLETION-OF-COMPLEX COMPLETION-OF-DENOMINATOR COMPLETION-OF-IMAGPART COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL COMPLETION-OF-NUMERATOR COMPLETION-OF-REALPART COMPLETION-OF-SYMBOL-NAME COMPLETION-OF-SYMBOL-PACKAGE-NAME COMPLETION-OF-UNARY-/ COMPLETION-OF-UNARY-MINUS COMPLEX COMPLEX-0 COMPLEX-DEFINITION COMPLEX-EQUAL COMPLEX-IMPLIES1 COMPLEX-RATIONALP COMPLEXP COMPRESS1 COMPRESS11 COMPRESS2 COMPRESS21 COMPRESS211 COMPUTE-APPLICABLE-METHODS COMPUTE-RESTARTS CONCATENATE CONCATENATED-STREAM CONCATENATED-STREAM-STREAMS COND COND-CLAUSESP COND-MACRO CONDITION CONJUGATE CONS CONS-EQUAL CONS-SUBTREES CONSP CONSP-ASSOC CONSP-ASSOC-EQ CONSTANTLY CONSTANTP CONTINUE CONTROL-ERROR COPY-ALIST COPY-LIST COPY-PPRINT-DISPATCH COPY-READTABLE COPY-SEQ COPY-STRUCTURE COPY-SYMBOL COPY-TREE COS COSH COUNT COUNT-IF COUNT-IF-NOT CTYPECASE CURRENT-PACKAGE CURRENT-THEORY CW CW-GSTACK DEBUG DECF DECLAIM DECLARATION DECLARE DECODE-FLOAT DECODE-UNIVERSAL-TIME DECREMENT-BIG-CLOCK DEFABBREV DEFAULT DEFAULT-*-1 DEFAULT-*-2 DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1 DEFAULT-<-2 DEFAULT-CAR DEFAULT-CDR DEFAULT-CHAR-CODE DEFAULT-COERCE-1 DEFAULT-COERCE-2 DEFAULT-COERCE-3 DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1 DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE DEFAULT-DEFUN-MODE-FROM-STATE DEFAULT-DENOMINATOR DEFAULT-IMAGPART DEFAULT-MEASURE-FUNCTION DEFAULT-NUMERATOR DEFAULT-REALPART DEFAULT-SYMBOL-NAME DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS DEFAULT-VERIFY-GUARDS-EAGERNESS DEFAULT-WELL-FOUNDED-RELATION DEFAXIOM DEFCHOOSE DEFCLASS DEFCONG DEFCONST DEFCONSTANT DEFDOC DEFEQUIV DEFEVALUATOR DEFEXEC DEFGENERIC DEFINE-COMPILER-MACRO DEFINE-CONDITION DEFINE-METHOD-COMBINATION DEFINE-MODIFY-MACRO DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP DEFINE-PC-MACRO DEFINE-SETF-EXPANDER DEFINE-SYMBOL-MACRO DEFLABEL DEFMACRO DEFMETHOD DEFPACKAGE DEFPARAMETER DEFPKG DEFREFINEMENT DEFSETF DEFSTOBJ DEFSTRUCT DEFSTUB DEFTHEORY DEFTHM DEFTHMD DEFTTAG DEFTYPE DEFUN DEFUN-NX DEFUN-SK DEFUND DEFUND-NX DEFUNS DEFVAR DELETE DELETE-DUPLICATES DELETE-FILE DELETE-IF DELETE-IF-NOT DELETE-PACKAGE DELETE-PAIR DENOMINATOR DEPOSIT-FIELD DESCRIBE DESCRIBE-OBJECT DESTRUCTURING-BIND DIGIT-CHAR DIGIT-CHAR-P DIGIT-TO-CHAR DIMENSIONS DIRECTORY DIRECTORY-NAMESTRING DISABLE DISABLE-FORCING DISABLEDP DISASSEMBLE DISTRIBUTIVITY DIVISION-BY-ZERO DO DO* DO-ALL-SYMBOLS DO-EXTERNAL-SYMBOLS DO-SYMBOLS DOC DOC! DOCS DOCUMENTATION DOLIST DOTIMES DOUBLE-FLOAT DOUBLE-FLOAT-EPSILON DOUBLE-FLOAT-NEGATIVE-EPSILON DOUBLE-REWRITE DPB DRIBBLE DUPLICATES DYNAMIC-EXTENT E/D E0-ORD-< E0-ORDINALP EC-CALL ECASE ECHO-STREAM ECHO-STREAM-INPUT-STREAM ECHO-STREAM-OUTPUT-STREAM ED EIGHTH ELIMINATE-DESTRUCTORS ELIMINATE-IRRELEVANCE ELT ENABLE ENABLE-FORCING ENCAPSULATE ENCODE-UNIVERSAL-TIME END-OF-FILE ENDP ENOUGH-NAMESTRING ENSURE-DIRECTORIES-EXIST ENSURE-GENERIC-FUNCTION EQ EQL EQLABLE-ALISTP EQLABLE-ALISTP-FORWARD-TO-ALISTP EQLABLE-LISTP EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP EQLABLEP EQLABLEP-RECOG EQUAL EQUAL-CHAR-CODE EQUALP ER ER-PROGN ER-PROGN-FN ERROR ETYPECASE EVAL EVAL-WHEN EVENP EVENS EVENT EVERY EXECUTABLE-COUNTERPART-THEORY EXP EXPLODE-ATOM EXPLODE-NONNEGATIVE-INTEGER EXPORT EXPT EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE EXTEND-32-BIT-INTEGER-STACK EXTEND-T-STACK EXTEND-WORLD EXTENDED-CHAR EXTRA-INFO FAST-ALIST-FREE FAST-ALIST-LEN FAST-ALIST-SUMMARY FBOUNDP FCEILING FDEFINITION FERTILIZE FFLOOR FGETPROP FIFTH FILE-AUTHOR FILE-CLOCK FILE-CLOCK-P FILE-CLOCK-P-FORWARD-TO-INTEGERP FILE-ERROR FILE-ERROR-PATHNAME FILE-LENGTH FILE-NAMESTRING FILE-POSITION FILE-STREAM FILE-STRING-LENGTH FILE-WRITE-DATE FILL FILL-POINTER FIND FIND-ALL-SYMBOLS FIND-CLASS FIND-IF FIND-IF-NOT FIND-METHOD FIND-PACKAGE FIND-RESTART FIND-SYMBOL FINISH-OUTPUT FIRST FIRST-N-AC FIX FIX-TRUE-LIST FIXNUM FLET FLOAT FLOAT-DIGITS FLOAT-PRECISION FLOAT-RADIX FLOAT-SIGN FLOATING-POINT-INEXACT FLOATING-POINT-INVALID-OPERATION FLOATING-POINT-OVERFLOW FLOATING-POINT-UNDERFLOW FLOATP FLOOR FLUSH-HONS-GET-HASH-TABLE-LINK FMAKUNBOUND FMS FMT FMT-TO-COMMENT-WINDOW FMT1 FORCE FORCE-OUTPUT FORMAT FORMATTER FOURTH FRESH-LINE FROUND FTRUNCATE FTYPE FUNCALL FUNCTION FUNCTION-KEYWORDS FUNCTION-LAMBDA-EXPRESSION FUNCTION-SYMBOLP FUNCTION-THEORY FUNCTIONP GCD GENERALIZE GENERIC-FUNCTION GENSYM GENTEMP GET GET-DECODED-TIME GET-DISPATCH-MACRO-CHARACTER GET-GLOBAL GET-INTERNAL-REAL-TIME GET-INTERNAL-RUN-TIME GET-MACRO-CHARACTER GET-OUTPUT-STREAM-STRING GET-PROPERTIES GET-SETF-EXPANSION GET-SLOW-ALIST-ACTION GET-TIMER GET-UNIVERSAL-TIME GETF GETHASH GETPROP-DEFAULT GETPROPS GETPROPS1 GLOBAL-TABLE GLOBAL-TABLE-CARS GLOBAL-TABLE-CARS1 GLOBAL-VAL GO GOOD-BYE GRANULARITY GRAPHIC-CHAR-P GROUND-ZERO HANDLER-BIND HANDLER-CASE HARD-ERROR HAS-PROPSP HAS-PROPSP1 HASH-TABLE HASH-TABLE-COUNT HASH-TABLE-P HASH-TABLE-REHASH-SIZE HASH-TABLE-REHASH-THRESHOLD HASH-TABLE-SIZE HASH-TABLE-TEST HEADER HELP HIDE HONS HONS-ACONS HONS-ACONS! HONS-CLEAR HONS-COPY HONS-EQUAL HONS-EQUAL-LITE HONS-GET HONS-RESIZE HONS-RESIZE-FN HONS-SHRINK-ALIST HONS-SHRINK-ALIST! HONS-SUMMARY HONS-WASH HOST-NAMESTRING I-AM-HERE ID IDATES IDENTITY IF IF* IFF IFF-IMPLIES-EQUAL-IMPLIES-1 IFF-IMPLIES-EQUAL-IMPLIES-2 IFF-IMPLIES-EQUAL-NOT IFF-IS-AN-EQUIVALENCE IFIX IGNORABLE IGNORE IGNORE-ERRORS ILLEGAL IMAGPART IMAGPART-COMPLEX IMMEDIATE-FORCE-MODEP IMPLIES IMPORT IMPROPER-CONSP IN-ARITHMETIC-THEORY IN-PACKAGE IN-THEORY INCF INCLUDE-BOOK INCOMPATIBLE INCREMENT-TIMER INDUCT INITIALIZE-INSTANCE INLINE INPUT-STREAM-P INSPECT INT= INTEGER INTEGER-0 INTEGER-1 INTEGER-ABS INTEGER-DECODE-FLOAT INTEGER-IMPLIES-RATIONAL INTEGER-LENGTH INTEGER-LISTP INTEGER-LISTP-FORWARD-TO-RATIONAL-LISTP INTEGER-STEP INTEGERP INTERACTIVE-STREAM-P INTERN INTERN$ INTERN-IN-PACKAGE-OF-SYMBOL INTERN-IN-PACKAGE-OF-SYMBOL-SYMBOL-NAME INTERNAL-TIME-UNITS-PER-SECOND INTERSECTION INTERSECTION-EQ INTERSECTION-THEORIES INTERSECTP-EQ INTERSECTP-EQUAL INVALID-METHOD-ERROR INVERSE-OF-* INVERSE-OF-+ INVISIBLE-FNS-TABLE INVOKE-DEBUGGER INVOKE-RESTART INVOKE-RESTART-INTERACTIVELY ISQRT KEYWORD KEYWORD-PACKAGE KEYWORD-VALUE-LISTP KEYWORD-VALUE-LISTP-ASSOC-KEYWORD KEYWORD-VALUE-LISTP-FORWARD-TO-TRUE-LISTP KEYWORDP KEYWORDP-FORWARD-TO-SYMBOLP KNOWN-PACKAGE-ALIST KNOWN-PACKAGE-ALISTP KNOWN-PACKAGE-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP LABELS LAMBDA LAMBDA-LIST-KEYWORDS LAMBDA-PARAMETERS-LIMIT LAST LCM LD LD-ERROR-ACTION LD-ERROR-TRIPLES LD-KEYWORD-ALIASES LD-POST-EVAL-PRINT LD-PRE-EVAL-FILTER LD-PRE-EVAL-PRINT LD-PROMPT LD-QUERY-CONTROL-ALIST LD-REDEFINITION-ACTION LD-SKIP-PROOFSP LD-VERBOSE LDB LDB-TEST LDIFF LEAST-NEGATIVE-DOUBLE-FLOAT LEAST-NEGATIVE-LONG-FLOAT LEAST-NEGATIVE-NORMALIZED-DOUBLE-FLOAT LEAST-NEGATIVE-NORMALIZED-LONG-FLOAT LEAST-NEGATIVE-NORMALIZED-SHORT-FLOAT LEAST-NEGATIVE-NORMALIZED-SINGLE-FLOAT LEAST-NEGATIVE-SHORT-FLOAT LEAST-NEGATIVE-SINGLE-FLOAT LEAST-POSITIVE-DOUBLE-FLOAT LEAST-POSITIVE-LONG-FLOAT LEAST-POSITIVE-NORMALIZED-DOUBLE-FLOAT LEAST-POSITIVE-NORMALIZED-LONG-FLOAT LEAST-POSITIVE-NORMALIZED-SHORT-FLOAT LEAST-POSITIVE-NORMALIZED-SINGLE-FLOAT LEAST-POSITIVE-SHORT-FLOAT LEAST-POSITIVE-SINGLE-FLOAT LEGAL-CASE-CLAUSESP LEN LEN-UPDATE-NTH LENGTH LET LET* LISP-IMPLEMENTATION-TYPE LISP-IMPLEMENTATION-VERSION LIST LIST* LIST*-MACRO LIST-ALL-PACKAGE-NAMES LIST-ALL-PACKAGE-NAMES-LST LIST-ALL-PACKAGES LIST-LENGTH LIST-MACRO LISTEN LISTP LOAD LOAD-LOGICAL-PATHNAME-TRANSLATIONS LOAD-TIME-VALUE LOCAL LOCALLY LOG LOGAND LOGANDC1 LOGANDC2 LOGBITP LOGCOUNT LOGEQV LOGIC LOGICAL-PATHNAME LOGICAL-PATHNAME-TRANSLATIONS LOGIOR LOGNAND LOGNOR LOGNOT LOGORC1 LOGORC2 LOGTEST LOGXOR LONG-FLOAT LONG-FLOAT-EPSILON LONG-FLOAT-NEGATIVE-EPSILON LONG-SITE-NAME LOOP LOOP-FINISH LOWER-CASE-P LOWER-CASE-P-CHAR-DOWNCASE LOWER-CASE-P-FORWARD-TO-ALPHA-CHAR-P LOWEST-TERMS LP MACHINE-INSTANCE MACHINE-TYPE MACHINE-VERSION MACRO-ALIASES MACRO-FUNCTION MACROEXPAND MACROEXPAND-1 MACROLET MAIN-TIMER MAIN-TIMER-TYPE-PRESCRIPTION MAKE-ARRAY MAKE-BROADCAST-STREAM MAKE-CHARACTER-LIST MAKE-CHARACTER-LIST-MAKE-CHARACTER-LIST MAKE-CONCATENATED-STREAM MAKE-CONDITION MAKE-DISPATCH-MACRO-CHARACTER MAKE-ECHO-STREAM MAKE-EVENT MAKE-FMT-BINDINGS MAKE-HASH-TABLE MAKE-INPUT-CHANNEL MAKE-INSTANCE MAKE-INSTANCES-OBSOLETE MAKE-LIST MAKE-LIST-AC MAKE-LOAD-FORM MAKE-LOAD-FORM-SAVING-SLOTS MAKE-METHOD MAKE-MV-NTHS MAKE-ORD MAKE-OUTPUT-CHANNEL MAKE-PACKAGE MAKE-PATHNAME MAKE-RANDOM-STATE MAKE-SEQUENCE MAKE-STRING MAKE-STRING-INPUT-STREAM MAKE-STRING-OUTPUT-STREAM MAKE-SYMBOL MAKE-SYNONYM-STREAM MAKE-TWO-WAY-STREAM MAKE-VAR-LST MAKE-VAR-LST1 MAKUNBOUND MAKUNBOUND-GLOBAL MAP MAP-INTO MAPC MAPCAN MAPCAR MAPCON MAPHASH MAPL MAPLIST MASK-FIELD MAX MAXIMUM-LENGTH MAY-NEED-SLASHES MBE MBT MEMBER MEMBER-EQ MEMBER-EQUAL MEMBER-IF MEMBER-IF-NOT MEMBER-SYMBOL-NAME MEMOIZE MEMOIZE-LET MEMOIZE-OFF MEMOIZE-ON MERGE MERGE-PATHNAMES METHOD METHOD-COMBINATION METHOD-COMBINATION-ERROR METHOD-QUALIFIERS MFC MIN MINIMAL-THEORY MINUSP MISMATCH MOD MONITOR MONITORED-RUNES MORE MORE! MORE-DOC MOST-NEGATIVE-DOUBLE-FLOAT MOST-NEGATIVE-FIXNUM MOST-NEGATIVE-LONG-FLOAT MOST-NEGATIVE-SHORT-FLOAT MOST-NEGATIVE-SINGLE-FLOAT MOST-POSITIVE-DOUBLE-FLOAT MOST-POSITIVE-FIXNUM MOST-POSITIVE-LONG-FLOAT MOST-POSITIVE-SHORT-FLOAT MOST-POSITIVE-SINGLE-FLOAT MUFFLE-WARNING MULTIPLE-VALUE-BIND MULTIPLE-VALUE-CALL MULTIPLE-VALUE-LIST MULTIPLE-VALUE-PROG1 MULTIPLE-VALUE-SETQ MULTIPLE-VALUES-LIMIT MUTUAL-RECURSION MUTUAL-RECURSION-GUARDP MV MV-LET MV-LIST MV-NTH NAME-CHAR NAMESTRING NATP NBUTLAST NCONC NEEDS-SLASHES NEWLINE NEXT-METHOD-P NFIX NIL NIL-IS-NOT-CIRCULAR NINTERSECTION NINTH NO-APPLICABLE-METHOD NO-DUPLICATESP NO-DUPLICATESP-EQUAL NO-NEXT-METHOD NONNEGATIVE-INTEGER-QUOTIENT NONNEGATIVE-PRODUCT NONZERO-IMAGPART NOT NOTANY NOTEVERY NOTINLINE NQTHM-TO-ACL2 NRECONC NREVERSE NSET-DIFFERENCE NSET-EXCLUSIVE-OR NSTRING-CAPITALIZE NSTRING-DOWNCASE NSTRING-UPCASE NSUBLIS NSUBST NSUBST-IF NSUBST-IF-NOT NSUBSTITUTE NSUBSTITUTE-IF NSUBSTITUTE-IF-NOT NTH NTH-0-CONS NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION NTH-ADD1 NTH-ALIASES NTH-UPDATE-NTH NTH-VALUE NTHCDR NULL NUMBER NUMBER-SUBTREES NUMBERP NUMERATOR NUNION O-FINP O-FIRST-COEFF O-FIRST-EXPT O-INFP O-P O-RST O< O<= O> O>= OBSERVATION ODDP ODDS OK-IF OOPS OPEN OPEN-CHANNEL-LISTP OPEN-CHANNEL1 OPEN-CHANNEL1-FORWARD-TO-TRUE-LISTP-AND-CONSP OPEN-CHANNELS-P OPEN-CHANNELS-P-FORWARD OPEN-INPUT-CHANNEL OPEN-INPUT-CHANNEL-ANY-P OPEN-INPUT-CHANNEL-ANY-P1 OPEN-INPUT-CHANNEL-P OPEN-INPUT-CHANNEL-P1 OPEN-INPUT-CHANNELS OPEN-OUTPUT-CHANNEL OPEN-OUTPUT-CHANNEL! OPEN-OUTPUT-CHANNEL-ANY-P OPEN-OUTPUT-CHANNEL-ANY-P1 OPEN-OUTPUT-CHANNEL-P OPEN-OUTPUT-CHANNEL-P1 OPEN-OUTPUT-CHANNELS OPEN-STREAM-P OPEN-TRACE-FILE OPTIMIZE OR OR-MACRO ORDERED-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-ADD-PAIR ORDERED-SYMBOL-ALISTP-ADD-PAIR-FORWARD ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP ORDERED-SYMBOL-ALISTP-GETPROPS ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR OTHERWISE OUR-DIGIT-CHAR-P OUTPUT-STREAM-P PACKAGE PACKAGE-ERROR PACKAGE-ERROR-PACKAGE PACKAGE-NAME PACKAGE-NICKNAMES PACKAGE-SHADOWING-SYMBOLS PACKAGE-USE-LIST PACKAGE-USED-BY-LIST PACKAGEP PAIRLIS PAIRLIS$ PAIRLIS2 PAND PARGS PARSE-ERROR PARSE-INTEGER PARSE-NAMESTRING PATHNAME PATHNAME-DEVICE PATHNAME-DIRECTORY PATHNAME-HOST PATHNAME-MATCH-P PATHNAME-NAME PATHNAME-TYPE PATHNAME-VERSION PATHNAMEP PBT PC PCB PCB! PCS PE PEEK-CHAR PEEK-CHAR$ PF PHASE PI PL PLET PLIST-WORLDP PLIST-WORLDP-FORWARD-TO-ASSOC-EQ-EQUAL-ALISTP PLUSP POP POP-TIMER POR POSITION POSITION-AC POSITION-EQ POSITION-EQ-AC POSITION-EQUAL POSITION-EQUAL-AC POSITION-IF POSITION-IF-NOT POSITIVE POSP POWER-EVAL PPRINT PPRINT-DISPATCH PPRINT-EXIT-IF-LIST-EXHAUSTED PPRINT-FILL PPRINT-INDENT PPRINT-LINEAR PPRINT-LOGICAL-BLOCK PPRINT-NEWLINE PPRINT-POP PPRINT-TAB PPRINT-TABULAR PPROGN PR PR! PREPROCESS PRIN1 PRIN1$ PRIN1-TO-STRING PRIN1-WITH-SLASHES PRIN1-WITH-SLASHES1 PRINC PRINC$ PRINC-TO-STRING PRINT PRINT-GV PRINT-NOT-READABLE PRINT-NOT-READABLE-OBJECT PRINT-OBJECT PRINT-OBJECT$ PRINT-RATIONAL-AS-DECIMAL PRINT-TIMER PRINT-UNREADABLE-OBJECT PROBE-FILE PROCLAIM PROG PROG* PROG1 PROG2 PROG2$ PROGN PROGRAM PROGRAM-ERROR PROGV PROOF-TREE PROOFS-CO PROPER-CONSP PROPS PROVE PROVIDE PSETF PSETQ PSEUDO-TERM-LISTP PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP PSEUDO-TERMP PSTACK PUFF PUFF* PUSH PUSH-TIMER PUSH-UNTOUCHABLE PUSHNEW PUT-ASSOC-EQ PUT-ASSOC-EQUAL PUT-GLOBAL PUTPROP QUOTE QUOTEP R-EQLABLE-ALISTP RANDOM RANDOM-STATE RANDOM-STATE-P RASSOC RASSOC-EQ RASSOC-EQUAL RASSOC-IF RASSOC-IF-NOT RATIO RATIONAL RATIONAL-IMPLIES1 RATIONAL-IMPLIES2 RATIONAL-LISTP RATIONAL-LISTP-FORWARD-TO-TRUE-LISTP RATIONALIZE RATIONALP RATIONALP-* RATIONALP-+ RATIONALP-EXPT-TYPE-PRESCRIPTION RATIONALP-IMPLIES-ACL2-NUMBERP RATIONALP-UNARY-- RATIONALP-UNARY-/ READ READ-ACL2-ORACLE READ-ACL2-ORACLE-PRESERVES-STATE-P1 READ-BYTE READ-BYTE$ READ-CHAR READ-CHAR$ READ-CHAR-NO-HANG READ-DELIMITED-LIST READ-FILE-LISTP READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP READ-FILE-LISTP1 READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP READ-FILES READ-FILES-P READ-FILES-P-FORWARD-TO-READ-FILE-LISTP READ-FROM-STRING READ-IDATE READ-LINE READ-OBJECT READ-PRESERVING-WHITESPACE READ-RUN-TIME READ-RUN-TIME-PRESERVES-STATE-P1 READ-SEQUENCE READABLE-FILE READABLE-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP READABLE-FILES READABLE-FILES-LISTP READABLE-FILES-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP READABLE-FILES-P READABLE-FILES-P-FORWARD-TO-READABLE-FILES-LISTP READER-ERROR READTABLE READTABLE-CASE READTABLEP REAL REAL/RATIONALP REALFIX REALP REALPART REALPART-COMPLEX REALPART-IMAGPART-ELIM REBUILD REDEF REDEF! REDEF+ REDUCE REINITIALIZE-INSTANCE REM REMF REMHASH REMOVE REMOVE-BINOP REMOVE-DEFAULT-HINTS REMOVE-DEFAULT-HINTS! REMOVE-DUPLICATES REMOVE-DUPLICATES-EQL REMOVE-DUPLICATES-EQUAL REMOVE-EQ REMOVE-EQUAL REMOVE-FIRST-PAIR REMOVE-IF REMOVE-IF-NOT REMOVE-INVISIBLE-FNS REMOVE-MACRO-ALIAS REMOVE-METHOD REMOVE-NTH-ALIAS REMOVE-UNTOUCHABLE REMOVE1 REMOVE1-EQ REMOVE1-EQUAL REMPROP RENAME-FILE RENAME-PACKAGE REPLACE REQUIRE RESET-LD-SPECIALS RESET-PREHISTORY REST RESTART RESTART-BIND RESTART-CASE RESTART-NAME RETRACT-WORLD RETRIEVE RETURN RETURN-FROM REVAPPEND REVERSE RFIX ROOM ROTATEF ROUND ROW-MAJOR-AREF RPLACA RPLACD SAFETY SATISFIES SBIT SCALE-FLOAT SCHAR SEARCH SECOND SEQUENCE SERIOUS-CONDITION SET SET-BACKCHAIN-LIMIT SET-BODY SET-BOGUS-DEFUN-HINTS-OK SET-BOGUS-MUTUAL-RECURSION-OK SET-CASE-SPLIT-LIMITATIONS SET-CBD SET-CHECKPOINT-SUMMARY-LIMIT SET-COMPILE-FNS SET-DEBUGGER-ENABLE SET-DEFAULT-BACKCHAIN-LIMIT SET-DEFAULT-HINTS SET-DEFAULT-HINTS! SET-DIFFERENCE SET-DIFFERENCE-EQ SET-DIFFERENCE-EQUAL SET-DIFFERENCE-THEORIES SET-DISPATCH-MACRO-CHARACTER SET-ENFORCE-REDUNDANCY SET-EQUALP-EQUAL SET-EXCLUSIVE-OR SET-GAG-MODE SET-GUARD-CHECKING SET-IGNORE-DOC-STRING-ERROR SET-IGNORE-OK SET-INHIBIT-OUTPUT-LST SET-INHIBIT-WARNINGS SET-INHIBITED-SUMMARY-TYPES SET-INVISIBLE-FNS-TABLE SET-IRRELEVANT-FORMALS-OK SET-LD-KEYWORD-ALIASES SET-LD-REDEFINITION-ACTION SET-LD-SKIP-PROOFS SET-LD-SKIP-PROOFSP SET-LET*-ABSTRACTION SET-LET*-ABSTRACTIONP SET-MACRO-CHARACTER SET-MATCH-FREE-DEFAULT SET-MATCH-FREE-ERROR SET-MEASURE-FUNCTION SET-NON-LINEAR SET-NON-LINEARP SET-NU-REWRITER-MODE SET-PARALLEL-EVALUATION SET-PPRINT-DISPATCH SET-PRINT-BASE SET-PRINT-CASE SET-PRINT-CLAUSE-IDS SET-RAW-MODE SET-RAW-MODE-ON! SET-RAW-PROOF-FORMAT SET-REWRITE-STACK-LIMIT SET-RULER-EXTENDERS SET-SAVED-OUTPUT SET-SLOW-ALIST-ACTION SET-STATE-OK SET-SYNTAX-FROM-CHAR SET-TAINTED-OK SET-TAINTED-OKP SET-TIMER SET-TRACE-EVISC-TUPLE SET-VERIFY-GUARDS-EAGERNESS SET-W SET-WELL-FOUNDED-RELATION SETF SETQ SEVENTH SGETPROP SHADOW SHADOWING-IMPORT SHARED-INITIALIZE SHIFTF SHORT-FLOAT SHORT-FLOAT-EPSILON SHORT-FLOAT-NEGATIVE-EPSILON SHORT-SITE-NAME SHOW-ACCUMULATED-PERSISTENCE SHOW-BDD SHOW-BODIES SHRINK-32-BIT-INTEGER-STACK SHRINK-T-STACK SIGNAL SIGNED-BYTE SIGNUM SIMPLE-ARRAY SIMPLE-BASE-STRING SIMPLE-BIT-VECTOR SIMPLE-BIT-VECTOR-P SIMPLE-CONDITION SIMPLE-CONDITION-FORMAT-ARGUMENTS SIMPLE-CONDITION-FORMAT-CONTROL SIMPLE-ERROR SIMPLE-STRING SIMPLE-STRING-P SIMPLE-TYPE-ERROR SIMPLE-VECTOR SIMPLE-VECTOR-P SIMPLE-WARNING SIMPLIFY SIN SINGLE-FLOAT SINGLE-FLOAT-EPSILON SINGLE-FLOAT-NEGATIVE-EPSILON SINH SIXTH SKIP-PROOFS SLEEP SLOT-BOUNDP SLOT-EXISTS-P SLOT-MAKUNBOUND SLOT-MISSING SLOT-UNBOUND SLOT-VALUE SOFTWARE-TYPE SOFTWARE-VERSION SOME SOME-SLASHABLE SORT SPACE SPECIAL SPECIAL-OPERATOR-P SPEED SQRT STABLE-SORT STABLE-UNDER-SIMPLIFICATIONP STANDARD STANDARD-CHAR STANDARD-CHAR-LISTP STANDARD-CHAR-LISTP-APPEND STANDARD-CHAR-LISTP-FORWARD-TO-CHARACTER-LISTP STANDARD-CHAR-P STANDARD-CHAR-P-NTH STANDARD-CLASS STANDARD-CO STANDARD-GENERIC-FUNCTION STANDARD-METHOD STANDARD-OBJECT STANDARD-OI STANDARD-STRING-ALISTP STANDARD-STRING-ALISTP-FORWARD-TO-ALISTP START-PROOF-TREE STATE STATE-GLOBAL-LET*-CLEANUP STATE-GLOBAL-LET*-GET-GLOBALS STATE-GLOBAL-LET*-PUT-GLOBALS STATE-P STATE-P-IMPLIES-AND-FORWARD-TO-STATE-P1 STATE-P1 STATE-P1-FORWARD STATE-P1-UPDATE-MAIN-TIMER STATE-P1-UPDATE-NTH-2-WORLD STEP STOP-PROOF-TREE STORAGE-CONDITION STORE-VALUE STREAM STREAM-ELEMENT-TYPE STREAM-ERROR STREAM-ERROR-STREAM STREAM-EXTERNAL-FORMAT STREAMP STRING STRING-APPEND STRING-APPEND-LST STRING-CAPITALIZE STRING-DOWNCASE STRING-DOWNCASE1 STRING-EQUAL STRING-EQUAL1 STRING-GREATERP STRING-IS-NOT-CIRCULAR STRING-LEFT-TRIM STRING-LESSP STRING-LISTP STRING-NOT-EQUAL STRING-NOT-GREATERP STRING-NOT-LESSP STRING-RIGHT-TRIM STRING-STREAM STRING-TRIM STRING-UPCASE STRING-UPCASE1 STRING/= STRING< STRING<-IRREFLEXIVE STRING<-L STRING<-L-ASYMMETRIC STRING<-L-IRREFLEXIVE STRING<-L-TRANSITIVE STRING<-L-TRICHOTOMY STRING<= STRING= STRING> STRING>= STRINGP STRINGP-SYMBOL-PACKAGE-NAME STRIP-CARS STRIP-CDRS STRUCTURE STRUCTURE-CLASS STRUCTURE-OBJECT STYLE-WARNING SUBLIS SUBSEQ SUBSEQ-LIST SUBSETP SUBSETP-EQUAL SUBST SUBST-IF SUBST-IF-NOT SUBSTITUTE SUBSTITUTE-AC SUBSTITUTE-IF SUBSTITUTE-IF-NOT SUBTYPEP SUMMARY SVREF SXHASH SYMBOL SYMBOL-< SYMBOL-<-ASYMMETRIC SYMBOL-<-IRREFLEXIVE SYMBOL-<-TRANSITIVE SYMBOL-<-TRICHOTOMY SYMBOL-ALISTP SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP SYMBOL-DOUBLET-LISTP SYMBOL-EQUALITY SYMBOL-FUNCTION SYMBOL-LISTP SYMBOL-LISTP-FORWARD-TO-TRUE-LISTP SYMBOL-MACROLET SYMBOL-NAME SYMBOL-NAME-INTERN-IN-PACKAGE-OF-SYMBOL SYMBOL-PACKAGE SYMBOL-PACKAGE-NAME SYMBOL-PLIST SYMBOL-VALUE SYMBOLP SYMBOLP-INTERN-IN-PACKAGE-OF-SYMBOL SYNONYM-STREAM SYNONYM-STREAM-SYMBOL SYNP SYNTAXP SYS-CALL SYS-CALL-STATUS T T-STACK T-STACK-LENGTH T-STACK-LENGTH1 TABLE TABLE-ALIST TAGBODY TAILP TAKE TAN TANH TENTH TERPRI THE THE-ERROR THE-FIXNUM THE-FIXNUM! THEORY THEORY-INVARIANT THIRD THM THROW TIME TIME$ TIMER-ALISTP TIMER-ALISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-SYMBOL-ALISTP TOGGLE-PC-MACRO TRACE TRACE! TRACE$ TRACE* TRANS TRANS1 TRANSLATE-LOGICAL-PATHNAME TRANSLATE-PATHNAME TREE-EQUAL TRICHOTOMY TRUE-LIST-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ TRUE-LISTP TRUE-LISTP-CADR-ASSOC-EQ-FOR-OPEN-CHANNELS-P TRUE-LISTP-UPDATE-NTH TRUENAME TRUNCATE TWO-WAY-STREAM TWO-WAY-STREAM-INPUT-STREAM TWO-WAY-STREAM-OUTPUT-STREAM TYPE TYPE-ERROR TYPE-ERROR-DATUM TYPE-ERROR-EXPECTED-TYPE TYPE-OF TYPECASE TYPED-IO-LISTP TYPED-IO-LISTP-FORWARD-TO-TRUE-LISTP TYPEP U UBT UBT! UNARY-- UNARY-/ UNARY-FUNCTION-SYMBOL-LISTP UNBOUND-SLOT UNBOUND-SLOT-INSTANCE UNBOUND-VARIABLE UNDEFINED-FUNCTION UNEXPORT UNICITY-OF-0 UNICITY-OF-1 UNINTERN UNION UNION-EQ UNION-EQUAL UNION-THEORIES UNIVERSAL-THEORY UNLESS UNMEMOIZE UNMONITOR UNREAD-CHAR UNSAVE UNSIGNED-BYTE UNTRACE UNTRACE$ UNUSE-PACKAGE UNWIND-PROTECT UPDATE-32-BIT-INTEGER-STACK UPDATE-ACL2-ORACLE UPDATE-ACL2-ORACLE-PRESERVES-STATE-P1 UPDATE-BIG-CLOCK-ENTRY UPDATE-FILE-CLOCK UPDATE-GLOBAL-TABLE UPDATE-IDATES UPDATE-INSTANCE-FOR-DIFFERENT-CLASS UPDATE-INSTANCE-FOR-REDEFINED-CLASS UPDATE-LIST-ALL-PACKAGE-NAMES-LST UPDATE-NTH UPDATE-OPEN-INPUT-CHANNELS UPDATE-OPEN-OUTPUT-CHANNELS UPDATE-READ-FILES UPDATE-T-STACK UPDATE-USER-STOBJ-ALIST UPDATE-USER-STOBJ-ALIST1 UPDATE-WRITTEN-FILES UPGRADED-ARRAY-ELEMENT-TYPE UPGRADED-COMPLEX-PART-TYPE UPPER-CASE-P UPPER-CASE-P-CHAR-UPCASE UPPER-CASE-P-FORWARD-TO-ALPHA-CHAR-P USE-PACKAGE USE-VALUE USER-HOMEDIR-PATHNAME USER-STOBJ-ALIST USER-STOBJ-ALIST1 VALUE-TRIPLE VALUES VALUES-LIST VARIABLE VECTOR VECTOR-POP VECTOR-PUSH VECTOR-PUSH-EXTEND VECTORP VERBOSE-PSTACK VERIFY VERIFY-GUARDS VERIFY-TERMINATION W WARN WARNING WARNING! WHEN WILD-PATHNAME-P WITH-ACCESSORS WITH-COMPILATION-UNIT WITH-CONDITION-RESTARTS WITH-HASH-TABLE-ITERATOR WITH-INPUT-FROM-STRING WITH-OPEN-FILE WITH-OPEN-STREAM WITH-OUTPUT WITH-OUTPUT-TO-STRING WITH-PACKAGE-ITERATOR WITH-SIMPLE-RESTART WITH-SLOTS WITH-STANDARD-IO-SYNTAX WORLD WORMHOLE WORMHOLE-EVAL WORMHOLE1 WRITABLE-FILE-LISTP WRITABLE-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP WRITABLE-FILE-LISTP1 WRITABLE-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITE WRITE-BYTE WRITE-BYTE$ WRITE-CHAR WRITE-LINE WRITE-SEQUENCE WRITE-STRING WRITE-TO-STRING WRITEABLE-FILES WRITEABLE-FILES-P WRITEABLE-FILES-P-FORWARD-TO-WRITABLE-FILE-LISTP WRITTEN-FILE WRITTEN-FILE-FORWARD-TO-TRUE-LISTP-AND-CONSP WRITTEN-FILE-LISTP WRITTEN-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP-AND-ALISTP WRITTEN-FILES WRITTEN-FILES-P WRITTEN-FILES-P-FORWARD-TO-WRITTEN-FILE-LISTP XARGS XXXJOIN Y-OR-N-P YES-OR-NO-P ZEROP ZIP ZP) ("ACL2-AGP" & &ALLOW-OTHER-KEYS &AUX &BODY &ENVIRONMENT &KEY &OPTIONAL &REST &WHOLE * ** *** *ACL2-EXPORTS* *BREAK-ON-SIGNALS* *COMMON-LISP-SPECIALS-AND-CONSTANTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE* *COMPILE-FILE-PATHNAME* *COMPILE-FILE-TRUENAME* *COMPILE-PRINT* *COMPILE-VERBOSE* *DEBUG-IO* *DEBUGGER-HOOK* *DEFAULT-PATHNAME-DEFAULTS* *ERROR-OUTPUT* *FEATURES* *GENSYM-COUNTER* *LOAD-PATHNAME* *LOAD-PRINT* *LOAD-TRUENAME* *LOAD-VERBOSE* *MACROEXPAND-HOOK* *MAIN-LISP-PACKAGE-NAME* *MODULES* *PACKAGE* *PRINT-ARRAY* *PRINT-BASE* *PRINT-CASE* *PRINT-CIRCLE* *PRINT-ESCAPE* *PRINT-GENSYM* *PRINT-LENGTH* *PRINT-LEVEL* *PRINT-LINES* *PRINT-MISER-WIDTH* *PRINT-PPRINT-DISPATCH* *PRINT-PRETTY* *PRINT-RADIX* *PRINT-READABLY* *PRINT-RIGHT-MARGIN* *QUERY-IO* *RANDOM-STATE* *READ-BASE* *READ-DEFAULT-FLOAT-FORMAT* *READ-EVAL* *READ-SUPPRESS* *READTABLE* *STANDARD-CHARS* *STANDARD-CI* *STANDARD-CO* *STANDARD-INPUT* *STANDARD-OI* *STANDARD-OUTPUT* *TERMINAL-IO* *TRACE-OUTPUT* + ++ +++ - / // /// /= 1+ 1- 32-BIT-INTEGER-LISTP 32-BIT-INTEGER-LISTP-FORWARD-TO-INTEGER-LISTP 32-BIT-INTEGER-STACK 32-BIT-INTEGER-STACK-LENGTH 32-BIT-INTEGER-STACK-LENGTH1 32-BIT-INTEGERP 32-BIT-INTEGERP-FORWARD-TO-INTEGERP < <-ON-OTHERS <= = > >= ?-FN @ ABORT ABORT! ABS ACCUMULATED-PERSISTENCE ACL2-COUNT ACL2-INPUT-CHANNEL-PACKAGE ACL2-NUMBERP ACL2-ORACLE ACL2-OUTPUT-CHANNEL-PACKAGE ACL2-PACKAGE ACONS ACOS ACOSH ACTIVE-RUNEP ADD-BINOP ADD-DEFAULT-HINTS ADD-DEFAULT-HINTS! ADD-INVISIBLE-FNS ADD-MACRO-ALIAS ADD-METHOD ADD-NTH-ALIAS ADD-PAIR ADD-PAIR-PRESERVES-ALL-BOUNDP ADD-TIMERS ADD-TO-SET-EQ ADD-TO-SET-EQL ADD-TO-SET-EQUAL ADJOIN ADJUST-ARRAY ADJUSTABLE-ARRAY-P ALISTP ALISTP-FORWARD-TO-TRUE-LISTP ALL-BOUNDP ALL-BOUNDP-PRESERVES-ASSOC ALL-VARS ALL-VARS1 ALL-VARS1-LST ALLOCATE-INSTANCE ALPHA-CHAR-P ALPHA-CHAR-P-FORWARD-TO-CHARACTERP ALPHANUMERICP AND AND-MACRO APPEND APPLY APROPOS APROPOS-LIST AREF AREF-32-BIT-INTEGER-STACK AREF-T-STACK AREF1 AREF2 ARGS ARITHMETIC-ERROR ARITHMETIC-ERROR-OPERANDS ARITHMETIC-ERROR-OPERATION ARRAY ARRAY-DIMENSION ARRAY-DIMENSION-LIMIT ARRAY-DIMENSIONS ARRAY-DISPLACEMENT ARRAY-ELEMENT-TYPE ARRAY-HAS-FILL-POINTER-P ARRAY-IN-BOUNDS-P ARRAY-RANK ARRAY-RANK-LIMIT ARRAY-ROW-MAJOR-INDEX ARRAY-TOTAL-SIZE ARRAY-TOTAL-SIZE-LIMIT ARRAY1P ARRAY1P-CONS ARRAY1P-FORWARD ARRAY1P-LINEAR ARRAY2P ARRAY2P-CONS ARRAY2P-FORWARD ARRAY2P-LINEAR ARRAYP ASET-32-BIT-INTEGER-STACK ASET-T-STACK ASET1 ASET2 ASH ASIN ASINH ASSERT ASSERT$ ASSIGN ASSOC ASSOC-ADD-PAIR ASSOC-EQ ASSOC-EQ-EQUAL ASSOC-EQ-EQUAL-ALISTP ASSOC-EQUAL ASSOC-IF ASSOC-IF-NOT ASSOC-KEYWORD ASSOC-STRING-EQUAL ASSOC2 ASSOCIATIVITY-OF-* ASSOCIATIVITY-OF-+ ASSUME ATAN ATANH ATOM ATOM-LISTP ATOM-LISTP-FORWARD-TO-TRUE-LISTP BASE-CHAR BASE-STRING BIG-CLOCK-ENTRY BIG-CLOCK-NEGATIVE-P BIGNUM BINARY-* BINARY-+ BINARY-APPEND BIND-FREE BINOP-TABLE BIT BIT-AND BIT-ANDC1 BIT-ANDC2 BIT-EQV BIT-IOR BIT-NAND BIT-NOR BIT-NOT BIT-ORC1 BIT-ORC2 BIT-VECTOR BIT-VECTOR-P BIT-XOR BLOCK BOOLE BOOLE-1 BOOLE-2 BOOLE-AND BOOLE-ANDC1 BOOLE-ANDC2 BOOLE-C1 BOOLE-C2 BOOLE-CLR BOOLE-EQV BOOLE-IOR BOOLE-NAND BOOLE-NOR BOOLE-ORC1 BOOLE-ORC2 BOOLE-SET BOOLE-XOR BOOLEAN BOOLEAN-LISTP BOOLEAN-LISTP-CONS BOOLEAN-LISTP-FORWARD BOOLEAN-LISTP-FORWARD-TO-SYMBOL-LISTP BOOLEANP BOOLEANP-CHARACTERP BOOLEANP-COMPOUND-RECOGNIZER BOTH-CASE-P BOUNDED-INTEGER-ALISTP BOUNDED-INTEGER-ALISTP-FORWARD-TO-EQLABLE-ALISTP BOUNDED-INTEGER-ALISTP2 BOUNDP BOUNDP-GLOBAL BOUNDP-GLOBAL1 BREAK BROADCAST-STREAM BROADCAST-STREAM-STREAMS BRR BRR@ BUILD-STATE1 BUILT-IN-CLASS BUTLAST BYTE BYTE-POSITION BYTE-SIZE CAAAAR CAAADR CAAAR CAADAR CAADDR CAADR CAAR CADAAR CADADR CADAR CADDAR CADDDR CADDR CADR CALL-ARGUMENTS-LIMIT CALL-METHOD CALL-NEXT-METHOD CAR CAR-CDR-ELIM CAR-CONS CASE CASE-LIST CASE-LIST-CHECK CASE-MATCH CASE-SPLIT CASE-TEST CATCH CBD CCASE CDAAAR CDAADR CDAAR CDADAR CDADDR CDADR CDAR CDDAAR CDDADR CDDAR CDDDAR CDDDDR CDDDR CDDR CDR CDR-CONS CDRN CEILING CELL-ERROR CELL-ERROR-NAME CERROR CERTIFY-BOOK CERTIFY-BOOK! CHANGE-CLASS CHAR CHAR-CODE CHAR-CODE-CODE-CHAR-IS-IDENTITY CHAR-CODE-LIMIT CHAR-CODE-LINEAR CHAR-DOWNCASE CHAR-EQUAL CHAR-GREATERP CHAR-INT CHAR-LESSP CHAR-NAME CHAR-NOT-EQUAL CHAR-NOT-GREATERP CHAR-NOT-LESSP CHAR-UPCASE CHAR/= CHAR< CHAR<= CHAR= CHAR> CHAR>= CHARACTER CHARACTER-LISTP CHARACTER-LISTP-APPEND CHARACTER-LISTP-COERCE CHARACTER-LISTP-FORWARD-TO-EQLABLE-LISTP CHARACTER-LISTP-REMOVE-DUPLICATES-EQL CHARACTER-LISTP-REVAPPEND CHARACTER-LISTP-STRING-DOWNCASE-1 CHARACTER-LISTP-STRING-UPCASE1-1 CHARACTERP CHARACTERP-CHAR-DOWNCASE CHARACTERP-CHAR-UPCASE CHARACTERP-NTH CHARACTERP-PAGE CHARACTERP-RUBOUT CHARACTERP-TAB CHECK-TYPE CHECK-VARS-NOT-FREE CHECKPOINT-FORCED-GOALS CIS CLASS CLASS-NAME CLASS-OF CLAUSE CLEAR-HASH-TABLES CLEAR-INPUT CLEAR-MEMOIZE-TABLE CLEAR-MEMOIZE-TABLES CLEAR-OUTPUT CLOSE CLOSE-INPUT-CHANNEL CLOSE-OUTPUT-CHANNEL CLOSE-TRACE-FILE CLOSURE CLRHASH CODE-CHAR CODE-CHAR-CHAR-CODE-IS-IDENTITY CODE-CHAR-TYPE COERCE COERCE-INVERSE-1 COERCE-INVERSE-2 COERCE-OBJECT-TO-STATE COERCE-STATE-TO-OBJECT COMMUTATIVITY-OF-* COMMUTATIVITY-OF-+ COMP COMPILATION-SPEED COMPILE COMPILE-FILE COMPILE-FILE-PATHNAME COMPILED-FUNCTION COMPILED-FUNCTION-P COMPILER-MACRO COMPILER-MACRO-FUNCTION COMPLEMENT COMPLETION-OF-* COMPLETION-OF-+ COMPLETION-OF-< COMPLETION-OF-CAR COMPLETION-OF-CDR COMPLETION-OF-CHAR-CODE COMPLETION-OF-CODE-CHAR COMPLETION-OF-COERCE COMPLETION-OF-COMPLEX COMPLETION-OF-DENOMINATOR COMPLETION-OF-IMAGPART COMPLETION-OF-INTERN-IN-PACKAGE-OF-SYMBOL COMPLETION-OF-NUMERATOR COMPLETION-OF-REALPART COMPLETION-OF-SYMBOL-NAME COMPLETION-OF-SYMBOL-PACKAGE-NAME COMPLETION-OF-UNARY-/ COMPLETION-OF-UNARY-MINUS COMPLEX COMPLEX-0 COMPLEX-DEFINITION COMPLEX-EQUAL COMPLEX-IMPLIES1 COMPLEX-RATIONALP COMPLEXP COMPRESS1 COMPRESS11 COMPRESS2 COMPRESS21 COMPRESS211 COMPUTE-APPLICABLE-METHODS COMPUTE-RESTARTS CONCATENATE CONCATENATED-STREAM CONCATENATED-STREAM-STREAMS COND COND-CLAUSESP COND-MACRO CONDITION CONJUGATE CONS CONS-EQUAL CONS-SUBTREES CONSP CONSP-ASSOC CONSP-ASSOC-EQ CONSTANTLY CONSTANTP CONTINUE CONTROL-ERROR COPY-ALIST COPY-LIST COPY-PPRINT-DISPATCH COPY-READTABLE COPY-SEQ COPY-STRUCTURE COPY-SYMBOL COPY-TREE COS COSH COUNT COUNT-IF COUNT-IF-NOT CTYPECASE CURRENT-PACKAGE CURRENT-THEORY CW CW-GSTACK DEBUG DECF DECLAIM DECLARATION DECLARE DECODE-FLOAT DECODE-UNIVERSAL-TIME DECREMENT-BIG-CLOCK DEFABBREV DEFAULT DEFAULT-*-1 DEFAULT-*-2 DEFAULT-+-1 DEFAULT-+-2 DEFAULT-<-1 DEFAULT-<-2 DEFAULT-CAR DEFAULT-CDR DEFAULT-CHAR-CODE DEFAULT-COERCE-1 DEFAULT-COERCE-2 DEFAULT-COERCE-3 DEFAULT-COMPILE-FNS DEFAULT-COMPLEX-1 DEFAULT-COMPLEX-2 DEFAULT-DEFUN-MODE DEFAULT-DEFUN-MODE-FROM-STATE DEFAULT-DENOMINATOR DEFAULT-IMAGPART DEFAULT-MEASURE-FUNCTION DEFAULT-NUMERATOR DEFAULT-REALPART DEFAULT-SYMBOL-NAME DEFAULT-SYMBOL-PACKAGE-NAME DEFAULT-UNARY-/ DEFAULT-UNARY-MINUS DEFAULT-VERIFY-GUARDS-EAGERNESS DEFAULT-WELL-FOUNDED-RELATION DEFAXIOM DEFCHOOSE DEFCLASS DEFCONG DEFCONST DEFCONSTANT DEFDOC DEFEQUIV DEFEVALUATOR DEFEXEC DEFGENERIC DEFINE-COMPILER-MACRO DEFINE-CONDITION DEFINE-METHOD-COMBINATION DEFINE-MODIFY-MACRO DEFINE-PC-ATOMIC-MACRO DEFINE-PC-HELP DEFINE-PC-MACRO DEFINE-SETF-EXPANDER DEFINE-SYMBOL-MACRO DEFLABEL DEFMACRO DEFMETHOD DEFPACKAGE DEFPARAMETER DEFPKG DEFREFINEMENT DEFSETF DEFSTOBJ DEFSTRUCT DEFSTUB DEFTHEORY DEFTHM DEFTHMD DEFTTAG DEFTYPE DEFUN DEFUN-NX DEFUN-SK DEFUND DEFUND-NX DEFUNS DEFVAR DELETE DELETE-DUPLICATES DELETE-FILE DELETE-IF DELETE-IF-NOT DELETE-PACKAGE DELETE-PAIR DENOMINATOR DEPOSIT-FIELD DESCRIBE DESCRIBE-OBJECT DESTRUCTURING-BIND DIGIT-CHAR DIGIT-CHAR-P DIGIT-TO-CHAR DIMENSIONS DIRECTORY DIRECTORY-NAMESTRING DISABLE DISABLE-FORCING DISABLEDP DISASSEMBLE DISTRIBUTIVITY DIVISION-BY-ZERO DO DO* DO-ALL-SYMBOLS DO-EXTERNAL-SYMBOLS DO-SYMBOLS DOC DOC! DOCS DOCUMENTATION DOLIST DOTIMES DOUBLE-FLOAT DOUBLE-FLOAT-EPSILON DOUBLE-FLOAT-NEGATIVE-EPSILON DOUBLE-REWRITE DPB DRIBBLE DUPLICATES DYNAMIC-EXTENT E/D E0-ORD-< E0-ORDINALP EC-CALL ECASE ECHO-STREAM ECHO-STREAM-INPUT-STREAM ECHO-STREAM-OUTPUT-STREAM ED EIGHTH ELIMINATE-DESTRUCTORS ELIMINATE-IRRELEVANCE ELT ENABLE ENABLE-FORCING ENCAPSULATE ENCODE-UNIVERSAL-TIME END-OF-FILE ENDP ENOUGH-NAMESTRING ENSURE-DIRECTORIES-EXIST ENSURE-GENERIC-FUNCTION EQ EQL EQLABLE-ALISTP EQLABLE-ALISTP-FORWARD-TO-ALISTP EQLABLE-LISTP EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP EQLABLEP EQLABLEP-RECOG EQUAL EQUAL-CHAR-CODE EQUALP ER ER-PROGN ER-PROGN-FN ERROR ETYPECASE EVAL EVAL-WHEN EVENP EVENS EVENT EVERY EXECUTABLE-COUNTERPART-THEORY EXP EXPLODE-ATOM EXPLODE-NONNEGATIVE-INTEGER EXPORT EXPT EXPT-TYPE-PRESCRIPTION-NON-ZERO-BASE EXTEND-32-BIT-INTEGER-STACK EXTEND-T-STACK EXTEND-WORLD EXTENDED-CHAR EXTRA-INFO FAST-ALIST-FREE FAST-ALIST-LEN FAST-ALIST-SUMMARY FBOUNDP FCEILING FDEFINITION FERTILIZE FFLOOR FGETPROP FIFTH FILE-AUTHOR FILE-CLOCK FILE-CLOCK-P FILE-CLOCK-P-FORWARD-TO-INTEGERP FILE-ERROR FILE-ERROR-PATHNAME FILE-LENGTH FILE-NAMESTRING FILE-POSITION FILE-STREAM FILE-STRING-LENGTH FILE-WRITE
[all...]
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dacl2_packageScript.sml859 ("WRITE-BYTE$", "ACL2-USER", "ACL2"),
1235 ("FILE-WRITE-DATE", "ACL2-USER", "COMMON-LISP"),
1835 ("WRITE", "ACL2-USER", "COMMON-LISP"),
1837 ("WRITE-BYTE", "ACL2-USER", "COMMON-LISP"),
1839 ("WRITE-CHAR", "ACL2-USER", "COMMON-LISP"),
1841 ("WRITE-LINE", "ACL2-USER", "COMMON-LISP"),
1843 ("WRITE-SEQUENCE", "ACL2-USER", "COMMON-LISP"),
1845 ("WRITE-STRING", "ACL2-USER", "COMMON-LISP"),
1847 ("WRITE-TO-STRING", "ACL2-USER", "COMMON-LISP"),
2213 ("FILE-WRITE
[all...]
H A Dhol_defaxiomsScript.sml3691 [oracles: DEFUN ACL2::WRITE-BYTE$, DISK_THM] [axioms: ] []
/seL4-l4v-master/HOL4/examples/acl2/tests/round-trip/gold/
H A Daxioms.sml3173 mkpair (mksym "COMMON-LISP" "FILE-WRITE-DATE") (mkpair (mksym "COMMON-LISP"
3549 mkpair (mksym "COMMON-LISP" "WRITE") (mkpair (mksym "COMMON-LISP"
3551 "WRITE-BYTE") (mkpair (mksym "COMMON-LISP"
3553 "WRITE-CHAR") (mkpair (mksym "COMMON-LISP" "UPGRADED-ARRAY-ELEMENT-TYPE") (
3554 mkpair (mksym "COMMON-LISP" "WRITE-LINE") (mkpair (mksym "COMMON-LISP"
3555 "UPGRADED-COMPLEX-PART-TYPE") (mkpair (mksym "COMMON-LISP" "WRITE-SEQUENCE") (
3557 "WRITE-STRING") (mkpair (mksym "COMMON-LISP" "USE-PACKAGE") (mkpair (mksym
3558 "COMMON-LISP" "WRITE-TO-STRING") (mkpair (mksym "COMMON-LISP" "USE-VALUE") (
9828 mkpair (mksym "ACL2" "WRITE-BYTE$") (mkpair (mksym "ACL2" "SHRINK-T-STACK") (
10055 mksym "ACL2" "LD-FN") (mkpair (mksym "ACL2" "WRITE
[all...]

Completed in 488 milliseconds