| /seL4-l4v-master/HOL4/src/real/ |
| H A D | realSimps.sml | 213 val r2 = rule o Q.INST [`m` |-> `NUMERAL (BIT2 m)`] value
|
| H A D | realaxScript.sml | 159 val r2 = mk r' value
|
| H A D | intrealScript.sml | 360 val r2 = rule o Q.INST [`m` |-> `NUMERAL (BIT2 m)`] value
|
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | patternMatchesLib.sml | |
| /seL4-l4v-master/HOL4/polyml/samplecode/Foreign/ |
| H A D | ForeignTest.c | 50 struct r2 { int n, m; }; struct
|
| /seL4-l4v-master/HOL4/src/AI/machine_learning/ |
| H A D | mlTreeNeuralNetwork.sml | 268 val r2 = map (fn x => x * x) r1 value
|
| /seL4-l4v-master/HOL4/src/floating-point/ |
| H A D | binary_ieeeScript.sml | 509 and r2 = float_to_real z value
535 and r2 = float_to_real z value
[all...] |
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/arm_hyp/sel4/sel4_arch/ |
| H A D | types.h | 21 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/ |
| H A D | types.h | 21 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/l4v/tools/c-parser/testfiles/ |
| H A D | jiraver443.c | 50 seL4_Word r2, r3, r4, r5, r6, r7, r14; member in struct:seL4_UserContext_
|
| H A D | jiraver434.c | 8 int r2, r3; member in struct:__anon117
|
| /seL4-l4v-master/l4v/camkes/glue-proofs/ |
| H A D | RPCTo.c | 199 r2 member in struct:__anon93
|
| H A D | RPCFrom.c | 200 r2 member in struct:__anon78
|
| H A D | EventTo.c | 199 r2 member in struct:__anon63
|
| H A D | EventFrom.c | 199 r2 member in struct:__anon51
|
| /seL4-l4v-master/HOL4/src/tfl/src/ |
| H A D | Defn.sml | 1229 val r2 = MATCH_MP (DISCH_ALL (LIST_CONJ r1)) Empty_thm value
|
| /seL4-l4v-master/HOL4/src/opentheory/ |
| H A D | OpenTheoryMap.sml | 47 val r2 = many (map (fn (name,(Thy,Name)) => {name=sto name,const={Thy=Thy,Name=Name}}) r) value
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | normalForms.sml | 428 val r2 = HO_REWR_CONV LEFT_AND_FORALL_THM; value
442 val r2 = HO_REWR_CONV (GSYM RIGHT_AND_FORALL_THM); value
581 val r2 = REWR_CONV RIGHT_OR_OVER_AND; value
|
| /seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
| H A D | Region.java | 75 public void combine(Region r2) { argument
80 public int spaceBetween(Region r2) { argument
86 public boolean touching(Region r2) { argument
|
| /seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/ |
| H A D | Region.java | 75 public void combine(Region r2) { argument
80 public int spaceBetween(Region r2) { argument
86 public boolean touching(Region r2) { argument
|
| /seL4-l4v-master/HOL4/tools-poly/poly/ |
| H A D | Binaryset.sml | 258 val r2 = split_gt cmpKey s2 v value
336 val r2 = split_gt cmpKey t v value
349 val r2 = split_gt cmpKey s v value
[all...] |
| /seL4-l4v-master/HOL4/src/ring/src/ |
| H A D | quote.sml | 132 let val (r2,a2) = dest_comb r1 in value
|
| /seL4-l4v-master/HOL4/src/portableML/poly/ |
| H A D | Intset.sml | 239 val r2 = split_gt s v value
258 val r2 = split_gt s v value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_opsScript.sml | 389 val r2 = save_thm("ARM_LISP_CONST" ^ int_to_string i ^ "_" ^ task, value
424 val r2 = save_thm("X86_LISP_CONST" ^ int_to_string i ^ "_" ^ task, value
457 val r2 = save_thm("PPC_LISP_CONST" ^ int_to_string i ^ "_" ^ task, value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 1805 val r2 = sse_logic 64 (bop,(BitsN.bits(63,0) x,BitsN.bits(63,0) x0)) value
1817 val r2 = sse_logic 32 (bop,(BitsN.bits(95,64) x,BitsN.bits(95,64) x0)) value
[all...] |