/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/isabelle/src/Pure/Admin/ |
H A D | build_doc.scala | 50 val res2 = 56 if (res2.ok) { 63 res2.rc
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_doc.scala | 50 val res2 = 56 if (res2.ok) { 63 res2.rc
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_synthesis_demoScript.sml | 31 part pivot x res1 res2 = 34 then part pivot (CDR x) (Dot (CAR x) res1) res2 35 else part pivot (CDR x) res1 (Dot (CAR x) res2) 36 else Dot res1 res2`
|
H A D | lisp_extractScript.sml | 65 ``(by ==> R_ev (y,e,fns1,io1,ok1) res2) /\ 70 (if isTrue ans1 then res2 else res3)``, 71 Q.SPEC_TAC (`res3`,`res3`) \\ Q.SPEC_TAC (`res2`,`res2`) 152 ``(b1 ==> R_ap (fc,FST res1,a,SND res1) res2) ==> 154 (b1 /\ b2 ==> R_ev (App fc el,a,fns,io,ok) res2)``, 155 Q.SPEC_TAC (`res2`,`res2`) \\ Q.SPEC_TAC (`res1`,`res1`) 377 (b2 ==> R_ev (e,FUNION (VarBind xs (FST res1)) a,SND res1) res2) ==> 379 R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) res2``, [all...] |
/seL4-l4v-master/seL4/include/arch/arm/arch/machine/ |
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
|
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
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | source_propertiesScript.sml | 554 eval_from k2 input prog = (res2,t2) ��� 561 ���res2 t2. eval env x (s with clock := k) = (res2,t2) ��� 563 (���e. res1 = Err e ��� ���e. res2 = Err e) ��� 564 ���x. res2 = Res x ��� res1 = Res x ��� 568 ���res2 t2. evals env xs (s with clock := k) = (res2,t2) ��� 570 (���e. res1 = Err e ��� ���e. res2 = Err e) ��� 571 ���x. res2 = Res x ��� res1 = Res x ��� 583 \\ reverse (Cases_on ���res2���) \\ f [all...] |
H A D | x64asm_propertiesScript.sml | 161 ���k s res1 res2. NRC step k s res1 ��� NRC step k s res2 ��� res1 = res2
|
H A D | codegenScript.sml | 248 let res2 = c_exps (SND res1) (NONE::vs) fs xs in 249 (Append (FST res1) (FST res2), SND res2))
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | logrelScript.sml | 33 let (res2,s2) = sem env' (s' with clock := i') e' in 34 case (res1, res2) of 149 Cases_on `res2` >> 233 `?s2 res2. sem env (s with clock := i') e1 = (res2,s2)` by metis_tac [pair_CASES] >> 235 reverse (Cases_on `res2`) >> 240 `?s2' res2'. sem env' (s' with clock := i') e1' = (res2',s2')` by metis_tac [pair_CASES] >> 242 >- (Cases_on `res2'` >> 245 Cases_on `res2'` >> [all...] |
/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 76 val () = if (res1 andalso res2 andalso res3 andalso res4) then ()
|
/seL4-l4v-master/HOL4/examples/misc/ |
H A D | wardScript.sml | 215 fun check (p1, (_, (res1, _)), s1) (p2, (_, (res2, _)), s2) = 216 tml_eq (p1 @ nilf res1 @ s1) (p2 @ nilf res2 @ s2) 222 val ((pfx1, (_, (res1, th1)), sfx1), (pfx2, (_, (res2, th2)), sfx2)) = 234 listSyntax.is_nil res2 andalso List.all is_var pfx1 andalso
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | completion.scala | 38 case (result1 @ Some(res1), Some(res2)) => 39 if (res1.range != res2.range || res1.original != res2.original) result1 41 val items = (res1.items ::: res2.items).sorted(history.ordering)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | completion.scala | 38 case (result1 @ Some(res1), Some(res2)) => 39 if (res1.range != res2.range || res1.original != res2.original) result1 41 val items = (res1.items ::: res2.items).sorted(history.ordering)
|
/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 165 val () = if not (isSuccess res2) then 170 isSuccess res2 andalso
|
/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 158 val res3 = map dest_comb (filter (not o can dest_sep_hide) res2) 1096 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value 1099 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value 1103 val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2 1166 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] value 1169 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 value 1173 val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2 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/theorem-prover/milawa-prover/ |
H A D | milawa_execScript.sml | 204 !f args a ctxt fns ok res ok1 res2 ok2 ok3. 206 MR_ap (f,args,a,ctxt,fns,ok2) (res2,ok3) ==> (res = res2)` 208 !xs a ctxt fns ok res ok1 res2 ok2 ok3. 210 MR_evl (xs,a,ctxt,fns,ok2) (res2,ok3) ==> (res = res2)` 212 !x1 a ctxt fns ok res ok1 res2 ok2 ok3. 214 MR_ev (x1,a,ctxt,fns,ok2) (res2,ok3) ==> (res = res2)` 235 !f args a ctxt fns ok res ok1 res2 ok [all...] |
/seL4-l4v-master/HOL4/src/proofman/tests/ |
H A D | selftest.sml | 44 val res2 = ���^f (^f $ ^g $ ^x)��� value 45 val _ = if aconv res2 (mk_comb(f, fgx)) then OK() else die "FAILED"
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sml | 186 val res2 = conv2 tm' value 188 thenConvTrans tm res1 res2 295 val res2 as (lit'',th2) = literule2 lit' value 297 if Literal.equal lit lit' then res2
|
/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/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rule.sml | 186 val res2 = conv2 tm' value 188 thenConvTrans tm res1 res2 295 val res2 as (lit'',th2) = literule2 lit' value 297 if Literal.equal lit lit' then res2
|
/seL4-l4v-master/HOL4/src/res_quan/src/ |
H A D | Cond_rewrite.sml | 50 fun rr_compare ({redex=red1,residue=res1}, {redex=red2,residue=res2}) = 51 pair_compare(Term.compare,Term.compare) ((red1,res1),(red2,res2))
|
/seL4-l4v-master/HOL4/examples/computability/kolmog/ |
H A D | pfreefnsScript.sml | 778 drule_all_then (qx_choose_then ���res2��� strip_assume_tac) 781 Cases_on ���res1 ��� res2��� 782 >- (qpat_x_assum ���prefix_free { n2bl j | _ ��� j < res2}��� mp_tac >> 784 simp[] >> Cases_on ���res1 = res2��� >- metis_tac[] >> 785 ���res1 < res2��� by simp[] >> 787 ���res2 < res1��� by simp[] >>
|