/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/ |
H A D | readthm1Script.sml | 5 val read = save_thm("read", TRUTH); value
|
H A D | readthm2Script.sml | 7 val next_thm = save_thm("next_thm", CONJ read read)
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | HM_SimpleBuffer.sig | 4 val mkBuffer : unit -> {push : string -> unit, read : unit -> string,
|
H A D | HM_SimpleBuffer.sml | 7 fun read () = let function 15 {push = push, read = read, reset = reset}
|
H A D | QFRead.sml | 8 fun exhaust_lexer (read, close) = 11 case read () of 23 val read = QuoteFilter.makeLexer (fn n => TextIO.input instrm) qstate value 25 (read, (fn () => TextIO.closeIn instrm)) 33 val read = QuoteFilter.makeLexer str_read qstate value 35 (read, (fn () => ())) 41 val read = QuoteFilter.makeLexer (fn n => TextIO.input strm) qstate value 43 (read, (fn () => ())) 50 fun mkReaderEOF (read, close) = let 55 fun pull () = (s := read(); s [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | funCallScript.sml | 299 (w2n (read st SP) <= w2n (read st FP) - (12 + m)) /\ 300 locate_ge (read st FP) (12 + m)`; 320 Q.ABBREV_TAC `x = read st SP` THEN 321 Cases_on `w2n (read st FP) <= n + w2n (x:word32)` THEN 335 `!st l m k. locate_ge (read st SP) (k + LENGTH l) /\ 340 (isM (w2n (read st SP) - k - PRE (LENGTH l) + i)) = st '' (EL i l))`, 347 `locate_ge (read st1 SP) (LENGTH l) /\ standard_frame st1 m /\ 348 (w2n (regs ' 13) - k = w2n (read st1 SP))` by ALL_TAC THENL [ 370 `!st n. i > w2n (read s [all...] |
H A D | bigInstScript.sml | 49 (reade st (isR r) = read st (REG r)) /\ 51 (reade st (isV k) = read st (MEM (fp, NEG k))) /\ 70 (addr_of st (isV v) = w2n (read st FP) - v)`; 315 Q.ABBREV_TAC `y = w2n (read st FP)` THEN 394 ((run_cfl (BLK (push_one e)) st = st |# (isM (w2n (read st SP)), st '' e) |# (isR sp, st '' (isR sp) - 1w)) \/ 396 st |# (isM (w2n (read st SP)), st '' e) |# (isR 9, v) |# (isR sp, st '' (isR sp) - 1w))) 422 ~(addr_in_range st e (w2n (read st SP), w2n (read st SP) - k)) /\ valid_exp_1 e`; 426 `!st h l. valid_exp_3 h /\ locate_ge (read st SP) (SUC (LENGTH l)) 429 locate_ge (read st [all...] |
H A D | preARMScript.sml | 174 read (regs,mem) (exp:EXP) = 188 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (w2n (regs ' r) + k)) /\ 189 (read (regs,mem) (MEM (r,NEG k)) = mem ' (w2n (regs ' r) - k)) /\ 190 (read (regs,mem) (NCONST i) = n2w i) /\ 191 (read (regs,mem) (WCONST w) = w) /\ 192 (read (regs,mem) (REG r) = regs ' r)`, 242 MOV -> (cpsr, write s (THE dst) (read s (HD src))) 250 (* We must read values from the original state instead of the updated state *) 251 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read s (MEM(r,POS(i+1)))), i+1)) (s,0) src)) 254 (cpsr, write (FST (FOLDL (\(s1,i) reg. (write s1 reg (read [all...] |
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | GrammarAncestry.sml | 10 val (write, read) = 12 read = Lib.K Coding.StringData.decodel, 19 | SOME t => case read t of
|
/seL4-l4v-10.1.1/HOL4/src/datatype/theory_tests/ |
H A D | monofldBScript.sml | 7 val (write, read) = let 27 val msg = read()
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
H A D | PreListEncode.sml | 28 val bool_info = Option.valOf (TypeBase.read {Thy= "min", Tyop="bool"}); 37 val prod_info = Option.valOf (TypeBase.read {Thy="pair", Tyop="prod"}); 47 val sum_info = Option.valOf (TypeBase.read {Thy = "sum", Tyop = "sum"}); 58 Option.valOf (TypeBase.read {Thy = "option", Tyop = "option"}); 68 val list_info = Option.valOf (TypeBase.read {Thy = "list", Tyop = "list"}); 78 val num_info = Option.valOf (TypeBase.read {Thy = "num", Tyop = "num"}); 87 val one_info = Option.valOf (TypeBase.read {Thy = "one", Tyop = "one"});
|
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | basicSize.sml | 18 val bool_info = Option.valOf (TypeBase.read {Thy="min", Tyop = "bool"}); 32 (Option.valOf (TypeBase.read {Tyop="prod", Thy="pair"})) 40 (Option.valOf(TypeBase.read {Tyop="sum", Thy="sum"})); 46 val one_info = Option.valOf (TypeBase.read {Tyop="one",Thy="one"}) 58 val option_info = Option.valOf (TypeBase.read {Tyop="option", Thy="option"})
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | numa.scala | 21 def read(s: String): List[Int] = 29 space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | numa.scala | 21 def read(s: String): List[Int] = 29 space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | news.scala | 27 HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS"))))))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | news.scala | 27 HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS"))))))
|
/seL4-l4v-10.1.1/l4v/misc/filemerge/ |
H A D | unicode.py | 35 data = f.read().decode('utf-8')
|
H A D | xsymbol.py | 35 data = f.read()
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | preARMScript.sml | 182 read (regs,mem) (exp:EXP) = 196 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (MEM_ADDR (regs ' (n2w r)) + (n2w k))) /\ 197 (read (regs,mem) (MEM (r,NEG k)) = mem ' (MEM_ADDR (regs ' (n2w r)) - (n2w k))) /\ 198 (read (regs,mem) (NCONST i) = n2w i) /\ 199 (read (regs,mem) (WCONST w) = w) /\ 200 (read (regs,mem) (REG r) = regs ' (n2w r)) /\ 201 (read (regs,mem) (MEM (r,INR)) = ARB)`, 254 MOV => (cpsr, write s (THE dst) (read s (HD src))) 262 (* We must read values from the original state instead of the updated state *) 263 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | preARMScript.sml | 178 read (regs,mem) (exp:EXP) = 192 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (ADDR30 (regs ' (n2w r)) + (n2w k))) /\ 193 (read (regs,mem) (MEM (r,NEG k)) = mem ' (ADDR30 (regs ' (n2w r)) - (n2w k))) /\ 194 (read (regs,mem) (NCONST i) = n2w i) /\ 195 (read (regs,mem) (WCONST w) = w) /\ 196 (read (regs,mem) (REG r) = regs ' (n2w r)) /\ 197 (read (regs,mem) (MEM (r,INR)) = ARB)`, 250 MOV -> (cpsr, write s (THE dst) (read s (HD src))) 258 (* We must read values from the original state instead of the updated state *) 259 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read [all...] |
/seL4-l4v-10.1.1/HOL4/src/integer/testing/ |
H A D | readproblemfile.sig | 9 [readterm is] attempts to read a term from the stream is. If the stream 11 SOME (SOME t) if there is a term there to be read, or SOME NONE if 12 something was read, but if failed to parse as a term. The stream must 17 v. The very first term read is combined with the initial value v0.
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | FinalTag-sig.sml | 12 val read : string -> tag value
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
H A D | update_header.scala | 14 val text0 = File.read(path)
|
H A D | update_then.scala | 14 val text0 = File.read(path)
|
H A D | update_theorems.scala | 14 val text0 = File.read(path)
|