Searched refs:i2 (Results 101 - 114 of 114) sorted by relevance
12345
/seL4-l4v-master/HOL4/examples/ARM/v4/mlton/ |
H A D | evalML.sml | 444 val (nzcv2, (i2, (f2, m2))) = armML.DECODE_PSR cpsr2
|
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | Defn.sml | 918 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 D | logic.py | 355 def do_rewrite (x2 = x2_def, i2 = i2_def): 357 ass[(i.name, i.typ)] = i2
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | polyScript.sml | 598 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 D | Theory.sml | 177 fun make_thyid(s,i1,i2) = UID{name=s, sec=i1,usec=i2}
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_grammar.sml | 574 | (INFIX(STD_infix (i1, a1)), INFIX(STD_infix(i2, a2))) => 580 INFIX(STD_infix(rrunion i1 i2, a1))
|
H A D | parse_term.sml | 135 | (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 D | lisp_invScript.sml | 1998 \\ 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 D | integrationScript.sml | 1804 (!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 D | funCallScript.sml | 2020 `!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 D | Prim_rec.sml | 1142 and i2 = DISJS_CHAIN rule (ASSUME disj2) value 1143 in DISJ_CASES th (DISJ1 i1 (concl i2)) (DISJ2 (concl i1) i2)
|
H A D | Drule.sml | 2430 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 D | riscv.spec | 4937 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 D | jit_incrementalScript.sml | 2191 ``!xs l p cs t. iEXEC (xs,l,p,cs) t ==> ?i2. iFETCH p cs = SOME i2``,
|
Completed in 287 milliseconds
12345