Searched refs:i2 (Results 101 - 114 of 114) sorted by relevance

12345

/seL4-l4v-master/HOL4/examples/ARM/v4/mlton/
H A DevalML.sml444 val (nzcv2, (i2, (f2, m2))) = armML.DECODE_PSR cpsr2
/seL4-l4v-master/HOL4/src/tfl/src/
H A DDefn.sml918 fun tmi_eq (tm1,i1:int) (tm2,i2) = i1 = i2 andalso aconv tm1 tm2
1230 val i2 = MATCH_MP (DISCH_ALL i1) Empty_thm value
1233 ind = i2, SV=SV, stem=stem}
/seL4-l4v-master/graph-refine/
H A Dlogic.py355 def do_rewrite (x2 = x2_def, i2 = i2_def):
357 ass[(i.name, i.typ)] = i2
/seL4-l4v-master/HOL4/src/real/
H A DpolyScript.sml598 DISCH_THEN(X_CHOOSE_THEN (Term`N2:num`) (X_CHOOSE_TAC (Term`i2:num->real`))) THEN
601 EXISTS_TAC (Term`\n:num. if n < N1 then i1(n):real else i2(n - N1)`) THEN
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheory.sml177 fun make_thyid(s,i1,i2) = UID{name=s, sec=i1,usec=i2}
/seL4-l4v-master/HOL4/src/parse/
H A Dterm_grammar.sml574 | (INFIX(STD_infix (i1, a1)), INFIX(STD_infix(i2, a2))) =>
580 INFIX(STD_infix(rrunion i1 i2, a1))
H A Dparse_term.sml135 | (PM_LG i1, PM_LG i2) => if i1 = i2 then OK else Bad
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_invScript.sml1998 \\ Q.LIST_EXISTS_TAC [`m2`,`i2`,`TAKE (LENGTH ss) rs`,`DROP (LENGTH ss) rs`,`sym`,`~b`]
2001 \\ `ok_split_heap (r0::r1::r2::r3::r4::r5::rs,m2,i2,e)` by
2009 \\ `i2 <= e` by (FULL_SIMP_TAC std_ss [ok_split_heap_def])
2154 \\ Q.LIST_EXISTS_TAC [`m2`,`i2`,`TAKE (LENGTH ss) rs`,`DROP (LENGTH ss) rs`,`sym`,`b`]
2157 \\ `ok_split_heap (r0::r1::r2::r3::r4::r5::rs,m2,i2,e)` by
2164 \\ `i2 <= e` by (FULL_SIMP_TAC std_ss [ok_split_heap_def])
/seL4-l4v-master/HOL4/src/probability/
H A DintegrationScript.sml1804 (!i1 i2. i1 IN iset /\ i2 IN iset /\ ~(i1 = i2)
1805 ==> (interior(i1) INTER interior(i2) = {}))
2020 (!i1 i2. i1 IN iset /\ i2 IN iset /\ ~(i1 = i2)
2021 ==> (interior(i1) INTER interior(i2) = {})) /\
4345 abs(s1 - i1) < e / &4:real /\ abs(s2 - i2) < e / &4:real
4346 ==> abs(i1 - i2) <
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DfunCallScript.sml2020 `!x i1 i2 m2. locate_ge x (MAX i1 i2 + 13 + m2) ==>
2021 locate_ge x (MAX i1 i2 - i1 + 13 + i1 + m2)`,
/seL4-l4v-master/HOL4/src/1/
H A DPrim_rec.sml1142 and i2 = DISJS_CHAIN rule (ASSUME disj2) value
1143 in DISJ_CASES th (DISJ1 i1 (concl i2)) (DISJ2 (concl i1) i2)
H A DDrule.sml2430 val i2 = DISCH r_eq_r' (AP_TERM A (ASSUME r_eq_r')) value
2431 val thm = IMP_ANTISYM_RULE i1 i2
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/src/
H A Driscv.spec4937 case '000 ilo`2 ihi`4 i2`1 i3`1 rd 00' => ArithI(ADDI('01' : rd, 2, '00' : ihi : ilo : i3 : i2 : '00'))
4940 case '010 imi`3 rs1 i2`1 i6`1 rd 00' => Load( LW('01' : rd, '01' : rs1, '00000' : i6 : imi : i2 : '00' ))
4944 case '110 imi`3 rs1 i2`1 i6`1 rs2 00' => Store( SW('01' : rs1, '01' : rs2, '00000' : i6 : imi : i2 : '00' ))
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/
H A Djit_incrementalScript.sml2191 ``!xs l p cs t. iEXEC (xs,l,p,cs) t ==> ?i2. iFETCH p cs = SOME i2``,

Completed in 287 milliseconds

12345