| /seL4-l4v-10.1.1/HOL4/src/opentheory/compat/ |
| H A D | HOL4boolScript.sml | 20 val res2 = export(``~(p ==> q) ==> p``, value
|
| /seL4-l4v-10.1.1/HOL4/examples/rings/ |
| H A D | ringExamplesScript.sml | 19 val res2 = num_norm_conv `x+y+x : num`; value
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/test/ |
| H A D | performance.sml | 70 val res2 = runTestFun regexTestRunner2.test "IMPL_exec" tests; value
|
| /seL4-l4v-10.1.1/HOL4/src/boss/ |
| H A D | selftest.sml | 103 val res2 = test_assert (equal 2 o length o #1) value
|
| /seL4-l4v-10.1.1/HOL4/src/proofman/tests/ |
| H A D | selftest.sml | 44 val res2 = ���^f (^f $ ^g $ ^x)��� value
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/mosml/ |
| H A D | BuildCommand.sml | 152 val res2 = Systeml.systeml [fullPath [FileSys.getDir(), script']] value
|
| /seL4-l4v-10.1.1/l4v/spec/haskell/include/ |
| H A D | gic.h | 26 uint32_t res2[32]; /* [0x380, 0x400) */ member in struct:gic_dist_map_t
72 uint32_t res2[2]; /* [0x048, 0x050) */ member in struct:gic_cpu_iface_map
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | stack_analysisLib.sml | 91 val res2 = (pc,assum2,u2,NONE,get_pc_val post2) value
|
| H A D | derive_specsLib.sml | 528 val res2 = map (fn (nn,(th,i,x),y) => value
|
| /seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/seL4/include/arch/arm/arch/machine/ |
| H A D | gic_pl390.h | 79 uint32_t res2[32]; /* [0x380, 0x400) */ member in struct:gic_dist_map
125 uint32_t res2[2]; /* [0x048, 0x050) */ member in struct:gic_cpu_iface_map
261 uint32_t res2[3]; member in struct:gich_vcpu_ctrl_map
|
| /seL4-l4v-10.1.1/seL4/src/arch/arm/machine/ |
| H A D | l2c_310.c | 152 uint32_t res2[2]; member in struct:l2cc_map::__anon228
218 uint32_t res2[7]; member in struct:l2cc_map::__anon236
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
| H A D | ho_proverTools.sml | 438 val res2 = value
1082 val res2 = ski_discrim_unify pos_db (vars', eq2) value
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperCore.sml | 1115 val res2 = CHOOSE (y, lemma) res1 value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | ind_rel.sml | 1577 val res2 = delete_conjs1 pred body2 value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_opsScript.sml | 155 val res2 = filter (not o can dest_sep_cond) res value
1093 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value
1096 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value
1163 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value
1166 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value
1357 val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2) value
1404 val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2) value
1496 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] value
1548 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] value
1623 val res2 = prove_spec th imp def pre_tm post_tm value
1624 val res2 = RW [GSYM zLISP_raw] res2 value
1625 val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_FULL_GC] value
2473 val res2 = RW [GSYM zLISP_raw] result2 value
2474 val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_ERROR] value
2548 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] value
2700 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value
2703 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value
2923 val res2 = prove_spec th imp def pre_tm post_tm value
2927 val res2 = RW [lemma] res2 value
2962 val res2 = prove_spec th imp def pre_tm post_tm value
2966 val res2 = PURE_REWRITE_RULE [lemma] res2 value
3003 val res2 = prove_spec th imp def pre_tm post_tm value
3007 val res2 = RW [lemma] res2 value
[all...] |
| /seL4-l4v-10.1.1/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
|