Searched refs:READ (Results 1 - 25 of 30) sorted by relevance

12

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DFile.h24 enum FileMode { READ, WRITE }; enumerator in enum:FileMode
40 #define DEFAULTS fd(-1), mode(READ), buf(NULL), size(-1), pos(0), own_fd(true)
63 if (mode == READ)
73 if (m == READ){
84 assert(mode == READ);
103 if (mode == WRITE) setMode(READ);
107 if (mode == READ) setMode(WRITE);
111 assert(mode == READ);
H A DFile.C12 if (mode == READ) size = read(fd, buf, File_BufSize);
39 mode = has_r ? READ : WRITE;
44 if (mode == READ) size = read(fd, buf, File_BufSize);
H A DProof.C94 fp.setMode(READ);
145 fp.setMode(READ);
258 fp.setMode(READ);
345 fp.setMode(READ);
369 fp.setMode(READ);
/seL4-l4v-master/HOL4/src/monad/more_monads/
H A Dstate_monadLib.sml57 `READ f s`,
H A Dstate_transformerSyntax.sml62 val (read_tm, mk_read, dest_read, is_read) = s1 "READ"
H A Dstate_transformerScript.sml58 (READ : ('state -> 'a) -> ('a, 'state) M) f = \s. (f s, s)`;
H A DerrorStateMonadScript.sml50 (READ : ('state -> 'a) -> ('a, 'state) M) f = \s. SOME (f s, s)`;
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DIRSyntax.sml346 datatype ACCESS = READ | WRITE | PUSH | POP
359 fun ch_mode (UNKNOWN,UNKNOWN) READ = (INPUT,UNKNOWN)
360 | ch_mode (m,UNKNOWN) READ = (INPUT, UNKNOWN)
363 | ch_mode (m,OUTPUT) READ = (m,INSTACK)
364 | ch_mode (m,INSTACK) READ = (m,INSTACK)
376 ( List.map (fn exp => update_mode exp READ) src1;
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DIRSyntax.sml338 datatype ACCESS = READ | WRITE | PUSH | POP
351 fun ch_mode (UNKNOWN,UNKNOWN) READ = (INPUT,UNKNOWN)
352 | ch_mode (m,UNKNOWN) READ = (INPUT, UNKNOWN)
355 | ch_mode (m,OUTPUT) READ = (m,INSTACK)
356 | ch_mode (m,INSTACK) READ = (m,INSTACK)
368 ( List.map (fn exp => update_mode exp READ) src1;
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DIRSyntax.sml338 datatype ACCESS = READ | WRITE | PUSH | POP
351 fun ch_mode (UNKNOWN,UNKNOWN) READ = (INPUT,UNKNOWN)
352 | ch_mode (m,UNKNOWN) READ = (INPUT, UNKNOWN)
355 | ch_mode (m,OUTPUT) READ = (m,INSTACK)
356 | ch_mode (m,INSTACK) READ = (m,INSTACK)
368 ( List.map (fn exp => update_mode exp READ) src1;
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A DPKGS.sml61 ("*READ-BASE*" , "ACL2" , "COMMON-LISP"),
63 ("*READ-DEFAULT-FLOAT-FORMAT*" , "ACL2" , "COMMON-LISP"),
65 ("*READ-EVAL*" , "ACL2" , "COMMON-LISP"),
67 ("*READ-SUPPRESS*" , "ACL2" , "COMMON-LISP"),
729 ("READ-CHAR" , "ACL2" , "COMMON-LISP"),
731 ("READ-CHAR-NO-HANG" , "ACL2" , "COMMON-LISP"),
733 ("READ-DELIMITED-LIST" , "ACL2" , "COMMON-LISP"),
735 ("READ-FROM-STRING" , "ACL2" , "COMMON-LISP"),
737 ("READ-LINE" , "ACL2" , "COMMON-LISP"),
739 ("READ
[all...]
H A Dhol_defaxiomsScript.sml2973 [oracles: DEFUN ACL2::READ-FILES, DISK_THM] [axioms: ] []
2978 [oracles: DEFUN ACL2::UPDATE-READ-FILES, DISK_THM] [axioms: ] []
3135 [oracles: DEFUN ACL2::READ-FILE-LISTP1, DISK_THM] [axioms: ] []
3145 [oracles: DEFUN ACL2::READ-FILE-LISTP, DISK_THM] [axioms: ] []
3152 [oracles: DEFUN ACL2::READ-FILES-P] [axioms: ] []
3803 [oracles: DEFUN ACL2::READ-CHAR$, DISK_THM] [axioms: ] []
3823 [oracles: DEFUN ACL2::READ-BYTE$, DISK_THM] [axioms: ] []
3835 [oracles: DEFUN ACL2::READ-OBJECT, DISK_THM] [axioms: ] []
4054 [oracles: DEFUN ACL2::READ-IDATE, DISK_THM] [axioms: ] []
4063 [oracles: DEFUN ACL2::READ
[all...]
H A Daxioms.ml2973 mkpair (mksym "COMMON-LISP" "*READ-BASE*") (mkpair (mksym "COMMON-LISP" "**") (
2974 mkpair (mksym "COMMON-LISP" "*READ-DEFAULT-FLOAT-FORMAT*") (mkpair (mksym
2975 "COMMON-LISP" "***") (mkpair (mksym "COMMON-LISP" "*READ-EVAL*") (mkpair (
2977 "*READ-SUPPRESS*") (mkpair (mksym "COMMON-LISP" "*COMPILE-FILE-PATHNAME*") (
3384 mkpair (mksym "COMMON-LISP" "READ-CHAR") (mkpair (mksym "COMMON-LISP"
3385 "PPRINT-TABULAR") (mkpair (mksym "COMMON-LISP" "READ-CHAR-NO-HANG") (mkpair (
3387 "READ-DELIMITED-LIST") (mkpair (mksym "COMMON-LISP" "PRIN1-TO-STRING") (
3388 mkpair (mksym "COMMON-LISP" "READ-FROM-STRING") (mkpair (mksym "COMMON-LISP"
3389 "PRINC") (mkpair (mksym "COMMON-LISP" "READ-LINE") (mkpair (mksym
3391 "READ
[all...]
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dkpa-v2-9-3.ml429 ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"),
536 ("READ-BYTE$", "ACL2-USER", "ACL2"),
537 ("READ-CHAR$", "ACL2-USER", "ACL2"),
538 ("READ-FILE-LISTP", "ACL2-USER", "ACL2"),
539 ("READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"),
540 ("READ-FILE-LISTP1", "ACL2-USER", "ACL2"),
541 ("READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
542 ("READ-FILES", "ACL2-USER", "ACL2"),
543 ("READ-FILES-P", "ACL2-USER", "ACL2"),
544 ("READ
[all...]
H A Dacl2_packageScript.sml540 ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"),
647 ("READ-BYTE$", "ACL2-USER", "ACL2"),
648 ("READ-CHAR$", "ACL2-USER", "ACL2"),
649 ("READ-FILE-LISTP", "ACL2-USER", "ACL2"),
650 ("READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"),
651 ("READ-FILE-LISTP1", "ACL2-USER", "ACL2"),
652 ("READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
653 ("READ-FILES", "ACL2-USER", "ACL2"),
654 ("READ-FILES-P", "ACL2-USER", "ACL2"),
655 ("READ
[all...]
H A Dhol_defaxioms_proofsScript.sml2125 csym "*READ-BASE*"; csym "**";
2126 csym "*READ-DEFAULT-FLOAT-FORMAT*"; csym "***";
2127 csym "*READ-EVAL*"; csym "*BREAK-ON-SIGNALS*";
2128 csym "*READ-SUPPRESS*";
2460 csym "PPRINT-TAB"; csym "READ-CHAR";
2461 csym "PPRINT-TABULAR"; csym "READ-CHAR-NO-HANG";
2462 csym "PRIN1"; csym "READ-DELIMITED-LIST";
2463 csym "PRIN1-TO-STRING"; csym "READ-FROM-STRING";
2464 csym "PRINC"; csym "READ-LINE";
2466 csym "READ
[all...]
H A Dhol_defaxiomsScript.sml2931 [oracles: DEFUN ACL2::READ-FILES, DISK_THM] [axioms: ] []
2936 [oracles: DEFUN ACL2::UPDATE-READ-FILES, DISK_THM] [axioms: ] []
3093 [oracles: DEFUN ACL2::READ-FILE-LISTP1, DISK_THM] [axioms: ] []
3103 [oracles: DEFUN ACL2::READ-FILE-LISTP, DISK_THM] [axioms: ] []
3110 [oracles: DEFUN ACL2::READ-FILES-P] [axioms: ] []
3761 [oracles: DEFUN ACL2::READ-CHAR$, DISK_THM] [axioms: ] []
3781 [oracles: DEFUN ACL2::READ-BYTE$, DISK_THM] [axioms: ] []
3793 [oracles: DEFUN ACL2::READ-OBJECT, DISK_THM] [axioms: ] []
4012 [oracles: DEFUN ACL2::READ-IDATE, DISK_THM] [axioms: ] []
4021 [oracles: DEFUN ACL2::READ
[all...]
H A Ddefaxioms.lisp.trans.ml5175 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "READ-FILES") (
5184 "UPDATE-READ-FILES") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2"
5619 "READ-FILE-LISTP1") (mkpair (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP"
5660 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "READ-FILE-LISTP") (
5667 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "READ-FILE-LISTP1") (mkpair (
5670 "ACL2" "READ-FILE-LISTP") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
5677 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "READ-FILES-P") (
5679 mkpair (mksym "ACL2" "READ-FILE-LISTP") (mkpair (mksym "ACL2" "X") (mksym
5902 "READ-FILES-P") (mkpair (mkpair (mksym "ACL2" "READ
[all...]
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/
H A DPKGS.sml20 ("*READ-BASE*" , "ACL2" , "COMMON-LISP"),
22 ("*READ-DEFAULT-FLOAT-FORMAT*" , "ACL2" , "COMMON-LISP"),
24 ("*READ-EVAL*" , "ACL2" , "COMMON-LISP"),
26 ("*READ-SUPPRESS*" , "ACL2" , "COMMON-LISP"),
688 ("READ-CHAR" , "ACL2" , "COMMON-LISP"),
690 ("READ-CHAR-NO-HANG" , "ACL2" , "COMMON-LISP"),
692 ("READ-DELIMITED-LIST" , "ACL2" , "COMMON-LISP"),
694 ("READ-FROM-STRING" , "ACL2" , "COMMON-LISP"),
696 ("READ-LINE" , "ACL2" , "COMMON-LISP"),
698 ("READ
[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
[all...]
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dacl2_packageScript.sml540 ("NTH-0-READ-RUN-TIME-TYPE-PRESCRIPTION", "ACL2-USER", "ACL2"),
647 ("READ-BYTE$", "ACL2-USER", "ACL2"),
648 ("READ-CHAR$", "ACL2-USER", "ACL2"),
649 ("READ-FILE-LISTP", "ACL2-USER", "ACL2"),
650 ("READ-FILE-LISTP-FORWARD-TO-TRUE-LIST-LISTP", "ACL2-USER", "ACL2"),
651 ("READ-FILE-LISTP1", "ACL2-USER", "ACL2"),
652 ("READ-FILE-LISTP1-FORWARD-TO-TRUE-LISTP-AND-CONSP", "ACL2-USER", "ACL2"),
653 ("READ-FILES", "ACL2-USER", "ACL2"),
654 ("READ-FILES-P", "ACL2-USER", "ACL2"),
655 ("READ
[all...]
H A Dhol_defaxiomsScript.sml2935 [oracles: DEFUN ACL2::READ-FILES, DISK_THM] [axioms: ] []
2940 [oracles: DEFUN ACL2::UPDATE-READ-FILES, DISK_THM] [axioms: ] []
3097 [oracles: DEFUN ACL2::READ-FILE-LISTP1, DISK_THM] [axioms: ] []
3107 [oracles: DEFUN ACL2::READ-FILE-LISTP, DISK_THM] [axioms: ] []
3114 [oracles: DEFUN ACL2::READ-FILES-P] [axioms: ] []
3765 [oracles: DEFUN ACL2::READ-CHAR$, DISK_THM] [axioms: ] []
3785 [oracles: DEFUN ACL2::READ-BYTE$, DISK_THM] [axioms: ] []
3797 [oracles: DEFUN ACL2::READ-OBJECT, DISK_THM] [axioms: ] []
4016 [oracles: DEFUN ACL2::READ-IDATE, DISK_THM] [axioms: ] []
4025 [oracles: DEFUN ACL2::READ
[all...]
/seL4-l4v-master/HOL4/Manual/Guide/
H A Dguide.tex138 \noindent Each of these subdirectories contains a {\tt READ-ME} file explaining
140 directories are advised to first read the appropriate {\tt READ-ME} files.
1545 \item{\tt READ-ME}: this should be a simple text file giving at least:
1554 Other items may be included, but the {\tt READ-ME} file should be kept brief.
/seL4-l4v-master/HOL4/examples/acl2/tests/round-trip/gold/
H A Daxioms.sml2973 mkpair (mksym "COMMON-LISP" "*READ-BASE*") (mkpair (mksym "COMMON-LISP" "**") (
2974 mkpair (mksym "COMMON-LISP" "*READ-DEFAULT-FLOAT-FORMAT*") (mkpair (mksym
2975 "COMMON-LISP" "***") (mkpair (mksym "COMMON-LISP" "*READ-EVAL*") (mkpair (
2977 "*READ-SUPPRESS*") (mkpair (mksym "COMMON-LISP" "*COMPILE-FILE-PATHNAME*") (
3384 mkpair (mksym "COMMON-LISP" "READ-CHAR") (mkpair (mksym "COMMON-LISP"
3385 "PPRINT-TABULAR") (mkpair (mksym "COMMON-LISP" "READ-CHAR-NO-HANG") (mkpair (
3387 "READ-DELIMITED-LIST") (mkpair (mksym "COMMON-LISP" "PRIN1-TO-STRING") (
3388 mkpair (mksym "COMMON-LISP" "READ-FROM-STRING") (mkpair (mksym "COMMON-LISP"
3389 "PRINC") (mkpair (mksym "COMMON-LISP" "READ-LINE") (mkpair (mksym
3391 "READ
[all...]
/seL4-l4v-master/isabelle/src/Pure/Thy/
H A Dsessions.scala964 using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>

Completed in 298 milliseconds

12