Searched refs:res2 (Results 1 - 25 of 45) sorted by relevance

12

/seL4-l4v-master/l4v/spec/haskell/include/
H A Dgic.h22 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 Dbuild_doc.scala50 val res2 =
56 if (res2.ok) {
63 res2.rc
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dbuild_doc.scala50 val res2 =
56 if (res2.ok) {
63 res2.rc
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_synthesis_demoScript.sml31 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 Dlisp_extractScript.sml65 ``(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 Dgic_v2.h61 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 Dgic_v3.h85 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 Dsource_propertiesScript.sml554 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 Dx64asm_propertiesScript.sml161 ���k s res1 res2. NRC step k s res1 ��� NRC step k s res2 ��� res1 = res2
H A DcodegenScript.sml248 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 DlogrelScript.sml33 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 Dperformance.sml70 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 DwardScript.sml215 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 Dcompletion.scala38 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 Dcompletion.scala38 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 Dl2c_310.c148 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 DBuildCommand.sml163 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 Dlisp_opsScript.sml156 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 Dmilawa_execScript.sml204 !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 Dselftest.sml44 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 DRule.sml186 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 DringExamplesScript.sml19 val res2 = num_norm_conv `x+y+x : num`; value
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DRule.sml186 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 DCond_rewrite.sml50 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 DpfreefnsScript.sml778 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[] >>

Completed in 126 milliseconds

12