/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 102 open my $INPUT, "$filename" or 110 while (my $line = <$INPUT>) { 250 close $INPUT;
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 102 open my $INPUT, "$filename" or 110 while (my $line = <$INPUT>) { 250 close $INPUT;
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | IRSyntax.sml | 347 datatype ROLE = UNKNOWN | INPUT | OUTPUT | INSTACK; 359 fun ch_mode (UNKNOWN,UNKNOWN) READ = (INPUT,UNKNOWN) 360 | ch_mode (m,UNKNOWN) READ = (INPUT, UNKNOWN) 395 val (ins, temps, outs) = (filter_inputs INPUT, filter_out_stack INSTACK, filter_out_stack OUTPUT);
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | IRSyntax.sml | 339 datatype ROLE = UNKNOWN | INPUT | OUTPUT | INSTACK; 351 fun ch_mode (UNKNOWN,UNKNOWN) READ = (INPUT,UNKNOWN) 352 | ch_mode (m,UNKNOWN) READ = (INPUT, UNKNOWN) 387 val (ins, temps, outs) = (filter_inputs INPUT, filter_out_stack INSTACK, filter_out_stack OUTPUT);
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | IRSyntax.sml | 339 datatype ROLE = UNKNOWN | INPUT | OUTPUT | INSTACK; 351 fun ch_mode (UNKNOWN,UNKNOWN) READ = (INPUT,UNKNOWN) 352 | ch_mode (m,UNKNOWN) READ = (INPUT, UNKNOWN) 387 val (ins, temps, outs) = (filter_inputs INPUT, filter_out_stack INSTACK, filter_out_stack OUTPUT);
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | kpa-v2-9-3.ml | 26 ("ACL2-INPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 137 ("CLOSE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 391 ("MAKE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 451 ("OPEN-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 452 ("OPEN-INPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 453 ("OPEN-INPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 454 ("OPEN-INPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 455 ("OPEN-INPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 456 ("OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 717 ("UPDATE-OPEN-INPUT [all...] |
H A D | hol_defaxioms_proofsScript.sml | 1854 ``"ACL2-INPUT-CHANNEL" = "ACL2-USER"``,``"ACL2-INPUT-CHANNEL" = "ACL2"``,``"ACL2-INPUT-CHANNEL" = "COMMON-LISP"``, 2037 [oracles: DEFAXIOM ACL2::ACL2-INPUT-CHANNEL-PACKAGE, DISK_THM] 2042 equal (symbol_package_name y) (str "ACL2-INPUT-CHANNEL")]) 2044 (str "ACL2-INPUT-CHANNEL")), 2050 time lookup_conv ``LOOKUP "ACL2-INPUT-CHANNEL" ACL2_PACKAGE_ALIST s0``); 2058 equal (symbol_package_name y) (str "ACL2-INPUT-CHANNEL")]) 2060 (str "ACL2-INPUT-CHANNEL"))``, 2131 csym "*STANDARD-INPUT*"; csy [all...] |
H A D | acl2_packageScript.sml | 137 ("ACL2-INPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 248 ("CLOSE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 502 ("MAKE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 562 ("OPEN-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 563 ("OPEN-INPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 564 ("OPEN-INPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 565 ("OPEN-INPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 566 ("OPEN-INPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 567 ("OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 828 ("UPDATE-OPEN-INPUT [all...] |
H A D | hol_defaxiomsScript.sml | 2826 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] [] 2831 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 3201 cons (asym "STANDARD-OI") (osym "STANDARD-OBJECT-INPUT-0"); 3310 (osym "STANDARD-OBJECT-INPUT-0"); 3621 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P1, DISK_THM] [axioms: ] [] 3635 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P] [axioms: ] [] 3665 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P1, DISK_THM] [axioms: ] [] 3676 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P] [axioms: ] [] 3709 [oracles: DEFUN ACL2::CLOSE-INPUT-CHANNEL, DISK_THM] [axioms: ] []
|
H A D | defaxioms.lisp.trans.ml | 5001 "OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "ST") (mksym 5009 "UPDATE-OPEN-INPUT-CHANNELS") (mkpair (mkpair (mksym "ACL2" "X") (mkpair ( 5751 "OPEN-INPUT-CHANNELS") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 5824 "STANDARD-OBJECT-INPUT-0")) (mkpair (mkpair (mksym "ACL2" "TAINTED-OKP") ( 5965 mkpair (mkpair (mksym "ACL2" "OPEN-INPUT-CHANNELS") (mkpair (mksym "ACL2" 6043 "STANDARD-OBJECT-INPUT-0")) (mkpair (mkpair (mksym "ACL2" "TAINTED-OKP") ( 6064 "COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "OPEN-INPUT-CHANNELS") (mkpair ( 6864 "OPEN-INPUT-CHANNEL-P1") (mkpair (mkpair (mksym "ACL2" "CHANNEL") (mkpair ( 6879 "OPEN-INPUT-CHANNELS") (mkpair (mksym "ACL2" "STATE-STATE") (mksym 6906 "OPEN-INPUT [all...] |
H A D | make_sexp.ml | 717 (* ("ACL2-INPUT-CHANNEL" NIL NIL NIL) *)
|
H A D | sexpScript.sml | 758 (* ("ACL2-INPUT-CHANNEL" NIL NIL NIL) *)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | PKGS.sml | 71 ("*STANDARD-INPUT*" , "ACL2" , "COMMON-LISP"), 235 ("CLEAR-INPUT" , "ACL2" , "COMMON-LISP"), 402 ("ECHO-STREAM-INPUT-STREAM" , "ACL2" , "COMMON-LISP"), 487 ("INPUT-STREAM-P" , "ACL2" , "COMMON-LISP"), 622 ("MAKE-STRING-INPUT-STREAM" , "ACL2" , "COMMON-LISP"), 960 ("TWO-WAY-STREAM-INPUT-STREAM" , "ACL2" , "COMMON-LISP"), 987 ("WITH-INPUT-FROM-STRING" , "ACL2" , "COMMON-LISP"), 1082 ("*STANDARD-INPUT*" , "ACL2-USER" , "COMMON-LISP"), 1118 ("ACL2-INPUT-CHANNEL-PACKAGE" , "ACL2-USER" , "ACL2"), 1388 ("CLEAR-INPUT" , "ACL [all...] |
H A D | hol_defaxiomsScript.sml | 2868 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] [] 2873 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 3243 cons (asym "STANDARD-OI") (osym "STANDARD-OBJECT-INPUT-0"); 3352 (osym "STANDARD-OBJECT-INPUT-0"); 3663 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P1, DISK_THM] [axioms: ] [] 3677 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P] [axioms: ] [] 3707 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P1, DISK_THM] [axioms: ] [] 3718 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P] [axioms: ] [] 3751 [oracles: DEFUN ACL2::CLOSE-INPUT-CHANNEL, DISK_THM] [axioms: ] []
|
H A D | axioms.ml | 2901 "ACL2-INPUT-CHANNEL-PACKAGE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 2979 "*COMPILE-FILE-TRUENAME*") (mkpair (mksym "COMMON-LISP" "*STANDARD-INPUT*") ( 3074 "CLEAR-INPUT") (mkpair (mksym "COMMON-LISP" "COPY-TREE") (mkpair (mksym 3172 "FILE-STRING-LENGTH") (mkpair (mksym "COMMON-LISP" "ECHO-STREAM-INPUT-STREAM") ( 3225 "GENERIC-FUNCTION") (mkpair (mksym "COMMON-LISP" "INPUT-STREAM-P") (mkpair ( 3318 "MAKE-STRING-INPUT-STREAM") (mkpair (mksym "COMMON-LISP" 3522 "TWO-WAY-STREAM-INPUT-STREAM") (mkpair (mksym "COMMON-LISP" "VECTOR") (mkpair ( 3539 mksym "COMMON-LISP" "WITH-INPUT-FROM-STRING") (mkpair (mksym "COMMON-LISP" 8590 mkpair (mkpair (mksym "ACL2" "INPUT-ARITY") (mkpair (mksym "ACL2" "X") (mksym 8727 "OPEN-INPUT [all...] |
H A D | sexpScript.sml | 758 (* ("ACL2-INPUT-CHANNEL" NIL NIL NIL) *)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | PKGS.sml | 30 ("*STANDARD-INPUT*" , "ACL2" , "COMMON-LISP"), 194 ("CLEAR-INPUT" , "ACL2" , "COMMON-LISP"), 361 ("ECHO-STREAM-INPUT-STREAM" , "ACL2" , "COMMON-LISP"), 446 ("INPUT-STREAM-P" , "ACL2" , "COMMON-LISP"), 581 ("MAKE-STRING-INPUT-STREAM" , "ACL2" , "COMMON-LISP"), 919 ("TWO-WAY-STREAM-INPUT-STREAM" , "ACL2" , "COMMON-LISP"), 946 ("WITH-INPUT-FROM-STRING" , "ACL2" , "COMMON-LISP"), 1041 ("*STANDARD-INPUT*" , "ACL2-USER" , "COMMON-LISP"), 1077 ("ACL2-INPUT-CHANNEL-PACKAGE" , "ACL2-USER" , "ACL2"), 1347 ("CLEAR-INPUT" , "ACL [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | acl2_packageScript.sml | 137 ("ACL2-INPUT-CHANNEL-PACKAGE", "ACL2-USER", "ACL2"), 248 ("CLOSE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 502 ("MAKE-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 562 ("OPEN-INPUT-CHANNEL", "ACL2-USER", "ACL2"), 563 ("OPEN-INPUT-CHANNEL-ANY-P", "ACL2-USER", "ACL2"), 564 ("OPEN-INPUT-CHANNEL-ANY-P1", "ACL2-USER", "ACL2"), 565 ("OPEN-INPUT-CHANNEL-P", "ACL2-USER", "ACL2"), 566 ("OPEN-INPUT-CHANNEL-P1", "ACL2-USER", "ACL2"), 567 ("OPEN-INPUT-CHANNELS", "ACL2-USER", "ACL2"), 828 ("UPDATE-OPEN-INPUT [all...] |
H A D | hol_defaxiomsScript.sml | 2830 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] [] 2835 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 3205 cons (asym "STANDARD-OI") (osym "STANDARD-OBJECT-INPUT-0"); 3314 (osym "STANDARD-OBJECT-INPUT-0"); 3625 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P1, DISK_THM] [axioms: ] [] 3639 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P] [axioms: ] [] 3669 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P1, DISK_THM] [axioms: ] [] 3680 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P] [axioms: ] [] 3713 [oracles: DEFUN ACL2::CLOSE-INPUT-CHANNEL, DISK_THM] [axioms: ] []
|
H A D | sexpScript.sml | 758 (* ("ACL2-INPUT-CHANNEL" NIL NIL NIL) *)
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/ |
H A D | holfoot_command_line.sml | 14 val s = "Syntax: holfoot [options] INPUT-FILES\n\n";
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/round-trip/gold/ |
H A D | axioms.sml | 2901 "ACL2-INPUT-CHANNEL-PACKAGE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 2979 "*COMPILE-FILE-TRUENAME*") (mkpair (mksym "COMMON-LISP" "*STANDARD-INPUT*") ( 3074 "CLEAR-INPUT") (mkpair (mksym "COMMON-LISP" "COPY-TREE") (mkpair (mksym 3172 "FILE-STRING-LENGTH") (mkpair (mksym "COMMON-LISP" "ECHO-STREAM-INPUT-STREAM") ( 3225 "GENERIC-FUNCTION") (mkpair (mksym "COMMON-LISP" "INPUT-STREAM-P") (mkpair ( 3318 "MAKE-STRING-INPUT-STREAM") (mkpair (mksym "COMMON-LISP" 3522 "TWO-WAY-STREAM-INPUT-STREAM") (mkpair (mksym "COMMON-LISP" "VECTOR") (mkpair ( 3539 mksym "COMMON-LISP" "WITH-INPUT-FROM-STRING") (mkpair (mksym "COMMON-LISP" 8590 mkpair (mkpair (mksym "ACL2" "INPUT-ARITY") (mkpair (mksym "ACL2" "X") (mksym 8727 "OPEN-INPUT [all...] |
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | selftest.sml | 1399 (* EXTENDING INPUT *)
|
/seL4-l4v-10.1.1/HOL4/tools/mllex/ |
H A D | mllex.sml | 390 (* INPUT.ML : Input w/ one character push back capability *)
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | ltl_to_automaton_formulaScript.sml | 2258 UNDISCH_NO_TAC 3 (*sv DS.SN IN INPUT ...*) THEN 2453 UNDISCH_NO_TAC 3 (*sv DS.SN IN INPUT ...*) THEN
|