| /seL4-l4v-master/seL4/include/arch/arm/arch/machine/ |
| H A D | gic_v3.h | 85 uint32_t res2; /* 0x0044 */ member in struct:gic_dist_map
132 uint32_t res2[8]; /* 0x0080 */ member in struct:gic_rdist_map
146 uint32_t res2[31]; /* 0x0104 */ member in struct:gic_rdist_sgi_ppi_map
|
| H A D | gic_v2.h | 61 uint32_t res2[32]; /* [0x380, 0x400) */ member in struct:gic_dist_map
107 uint32_t res2[2]; /* [0x048, 0x050) */ member in struct:gic_cpu_iface_map
220 uint32_t res2[3]; member in struct:gich_vcpu_ctrl_map
|
| /seL4-l4v-master/HOL4/src/boss/ |
| H A D | selftest.sml | 107 val res2 = test_assert (equal 2 o length o #1) value
|
| /seL4-l4v-master/HOL4/src/proofman/tests/ |
| H A D | selftest.sml | 44 val res2 = ���^f (^f $ ^g $ ^x)��� value
|
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | stack_analysisLib.sml | 99 val res2 = (pc,assum2,u2,NONE,get_pc_val post2) value
|
| H A D | derive_specsLib.sml | 584 val res2 = map (fn (nn,(th,i,x),y) => value
|
| /seL4-l4v-master/HOL4/src/opentheory/compat/ |
| H A D | HOL4boolScript.sml | 20 val res2 = export(``~(p ==> q) ==> p``, value
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | CooperCore.sml | 1120 val res2 = CHOOSE (y, lemma) res1 value
|
| /seL4-l4v-master/l4v/spec/haskell/include/ |
| H A D | gic.h | 22 uint32_t res2[32]; /* [0x380, 0x400) */ member in struct:gic_dist_map_t
68 uint32_t res2[2]; /* [0x048, 0x050) */ member in struct:gic_cpu_iface_map
|
| /seL4-l4v-master/seL4/src/arch/arm/machine/ |
| H A D | l2c_310.c | 148 uint32_t res2[2]; member in struct:l2cc_map::__anon241
214 uint32_t res2[7]; member in struct:l2cc_map::__anon249
|
| /seL4-l4v-master/HOL4/tools/Holmake/mosml/ |
| H A D | BuildCommand.sml | 163 val res2 = Systeml.systeml [script'] value
|
| /seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 773 val res2 = map (CONV_RULE (RATOR_CONV (RAND_CONV (K (GSYM sfb_thm))))) res value
|
| /seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
| H A D | ho_proverTools.sml | 448 val res2 = value
1089 val res2 = ski_discrim_unify pos_db (vars', eq2) value
|
| /seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
| H A D | Rule.sml | 186 val res2 = conv2 tm' value
295 val res2 as (lit'',th2) = literule2 lit' value
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Rule.sml | 186 val res2 = conv2 tm' value
295 val res2 as (lit'',th2) = literule2 lit' value
|
| /seL4-l4v-master/HOL4/src/quotient/examples/ |
| H A D | ind_rel.sml | 1565 val res2 = delete_conjs1 pred body2 value
|
| /seL4-l4v-master/HOL4/src/finite_maps/ |
| H A D | alist_treeLib.sml | 351 val res2 = timeit "map extract" (map (extract_test f rs)) (upto 1 1000) value
|
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_opsScript.sml | 156 val res2 = filter (not o can dest_sep_cond) res value
1096 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value
1099 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value
1166 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value
1169 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value
1360 val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2) value
1407 val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2) value
1499 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] value
1551 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] value
1626 val res2 = prove_spec th imp def pre_tm post_tm value
1627 val res2 = RW [GSYM zLISP_raw] res2 value
1628 val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_FULL_GC] value
2476 val res2 = RW [GSYM zLISP_raw] result2 value
2477 val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_ERROR] value
2551 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] value
2703 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value
2706 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value
2926 val res2 = prove_spec th imp def pre_tm post_tm value
2930 val res2 = RW [lemma] res2 value
2965 val res2 = prove_spec th imp def pre_tm post_tm value
2969 val res2 = PURE_REWRITE_RULE [lemma] res2 value
3006 val res2 = prove_spec th imp def pre_tm post_tm value
3010 val res2 = RW [lemma] res2 value
[all...] |
| /seL4-l4v-master/HOL4/examples/rings/ |
| H A D | ringExamplesScript.sml | 19 val res2 = num_norm_conv `x+y+x : num`; value
|
| /seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_opsScript.sml | 65 val res2 = filter (not o can dest_sep_cond) res value
|
| /seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/test/ |
| H A D | performance.sml | 70 val res2 = runTestFun regexTestRunner2.test "IMPL_exec" tests; value
|