/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | stack_analysisLib.sml | 130 val (i,(th1,i1,i2),thi2) = el 3 (rev thms) 133 fun approx_summary (i,(th1,i1,i2),thi2) = 135 then map tidy_up_summary (summary (i,(th1,i1,i2),thi2)) 137 val res = map tidy_up_summary (summary (i,(th1,i1,i2),thi2))
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/ |
H A D | omega_automaton_translationsScript.sml | 62 (\((s1, i1),(s2, i2)). (s1, i1, s2, i2) IN A.R /\ i1 SUBSET A.I /\ i2 SUBSET A.I) 262 !(S1 :'a set) (S2 :'a set) (i1 :'a set) (i2 :'a set). 264 (IS_TRANSITION A' S1 i1 S2 i2 <=> 265 (S2 = {s2 | s2 IN A'.S /\ ?s1. s1 IN S1 /\ IS_TRANSITION A (g s1) i1 (g s2) i2})))`; 354 INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') = 355 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 l', INPUT_RUN_STATE_UNION A i2 l'')` THEN1 ( 361 ((INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') INTER XP_USED_X_VARS A.R = 362 (INPUT_RUN_STATE_UNION A i2 [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | cheney_gcScript.sml | 635 (cheney_step(i,j,e,m) = (i2,j2,e2,m2)) ==> (e2 = e) /\ j <= j2 /\ 636 cheney_inv(b,b',i2,j2,j2,e2,f,m2,w,xx,r)``, 646 \\ Q.PAT_X_ASSUM `i + 1 = i2` (K ALL_TAC) 787 !i2 m2. (cheney(i,j,e,m) = (i2,m2)) ==> 788 cheney_inv(b,b',i2,i2,i2,e,f,m2,w,xx,r) /\ j <= i2) (i,j,e,m)``, 790 \\ `?i2 j [all...] |
H A D | arm_cheney_allocScript.sml | 198 \\ `?i2 e2 rs2 l2 u2 m2. cheney_alloc_gc (i,e,rs,l,u,m) = (i2,e2,rs2,l2,u2,m2)` by METIS_TAC [PAIR] 203 \\ `ok_state (i2,e2,rs2,l2,u2,m2)` by METIS_TAC [cheney_collector_spec,cheney_alloc_gc_def]
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | fmaptreeScript.sml | 94 (FTNode i1 f1 = FTNode i2 f2) <=> (i1 = i2) /\ (f1 = f2)
|
/seL4-l4v-master/HOL4/src/meson/src/ |
H A D | Canon_Port.sml | 26 fun tmi_eq (tm1,i1:int) (tm2,i2) = aconv tm1 tm2 andalso i1 = i2
|
H A D | mesonLib.sml | 54 fun tmi_eq (tm1,i1:int) (tm2,i2) = aconv tm1 tm2 andalso i1 = i2 646 fun eek (x1,(i1,th1)) (x2,(i2,th2)) = 647 (x1=x2) andalso (i1=i2) andalso thm_eq th1 th2 701 fun key_eq (i1,tm1) (i2,tm2) = aconv tm1 tm2 andalso i1 = i2
|
/seL4-l4v-master/HOL4/src/coalgebras/ |
H A D | coalgAxiomsScript.sml | 205 ((P,pf):'p system,i1,i2) (:'d) 208 hom i2 (C,cf) (P,pf) /\ restr (i1 o f) A = restr (i2 o g) A /\ 214 restr (u o i2) C = j2 244 Spushout A B C f g (P,i1,i2) (:'d) ==> 245 ?pf. Fpushout (A,af) (B,bf) (C,cf) f g ((P,pf),i1,i2) (:'d) 253 ���shom f A B /\ shom g A C /\ shom i1 B P /\ shom i2 C P��� 255 Cases_on ���restr (i1 o f) A = restr (i2 o g) A��� >> simp[] >> reverse eq_tac
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Map.sml | 578 | iterCompare kcmp vcmp (SOME i1) (SOME i2) = 579 keyIterCompare kcmp vcmp (readIterator i1) (readIterator i2) i1 i2 580 and keyIterCompare kcmp vcmp (k1,v1) (k2,v2) i1 i2 = 587 iterCompare kcmp vcmp (advanceIterator i1) (advanceIterator i2)
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | IRSyntax.sml | 110 let val (i1,i2) = (index_of_exp s1, index_of_exp s2) 112 if i1 > i2 then GREATER 113 else if i1 = i2 then EQUAL
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | IRSyntax.sml | 110 let val (i1,i2) = (index_of_exp s1, index_of_exp s2) 112 if i1 > i2 then GREATER 113 else if i1 = i2 then EQUAL
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | IRSyntax.sml | 110 let val (i1,i2) = (index_of_exp s1, index_of_exp s2) 112 if i1 > i2 then GREATER 113 else if i1 = i2 then EQUAL
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | ind_typeScript.sml | 247 !c1 i1 r1 c2 i2 r2. (CONSTR c1 i1 r1 :'a recspace = CONSTR c2 i2 r2) <=> 248 (c1 = c2) /\ (i1 = i2) /\ (r1 = r2)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_REMOVE_REDUNDANT.sml | 106 and mergefield(l1 as ((f1 as (i1, u1)) :: tl1), l2 as (f2 as (i2, u2)) ::tl2) = 107 if i1 < i2 then f1 :: mergefield(tl1, l2) 108 else if i1 > i2 then f2 :: mergefield(l1, tl2)
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | prog_ppcLib.sml | 215 | ((th1,i1,j1),SOME (th2,i2,j2)) => ((rename th1,i1,j1),SOME (rename th2,i2,j2))
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_seq_monadScript.sml | 321 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR]
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | ho_discrimTools.sml | 77 | (BVAR i1, BVAR i2) => i1 = i2
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | TheoryPP.sml | 215 val {theory as (name,i1,i2), parents=parents0, thydata, mldeps, axioms, 329 val {theory as (name,i1,i2), parents=parents0,
|
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | patternMatchesScript.sml | 943 (MAP2 (\i1 i2. i1 /\ i2) ip1 ip2)`; 948 (REDUNDANT_ROWS_INFOS_CONJ (i1 :: is1) (i2::is2) = 949 (i1 /\ i2) :: (REDUNDANT_ROWS_INFOS_CONJ is1 is2))``, 966 (MAP2 (\i1 i2. i1 \/ i2) ip1 ip2)`;
|
/seL4-l4v-master/HOL4/src/rational/ |
H A D | fracScript.sml | 787 * |- !f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==> 788 * (frac_sgn (frac_mul f1 f2) = i1 * i2) 792 (*val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==> (frac_sgn (frac_mul f1 f2) = i1 * i2)``,
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 963 | (SOME i1, SOME i2) => 966 and (k2,v2) = readIterator i2 976 and io2 = advanceIterator i2 989 | (SOME i1, SOME i2) => 992 and (k2,v2) = readIterator i2 998 and io2 = advanceIterator i2
|
H A D | Map.sml | 955 | (SOME i1, SOME i2) => 958 and (k2,v2) = readIterator i2 968 and io2 = advanceIterator i2 981 | (SOME i1, SOME i2) => 984 and (k2,v2) = readIterator i2 990 and io2 = advanceIterator i2
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 963 | (SOME i1, SOME i2) => 966 and (k2,v2) = readIterator i2 976 and io2 = advanceIterator i2 989 | (SOME i1, SOME i2) => 992 and (k2,v2) = readIterator i2 998 and io2 = advanceIterator i2
|
H A D | Map.sml | 955 | (SOME i1, SOME i2) => 958 and (k2,v2) = readIterator i2 968 and io2 = advanceIterator i2 981 | (SOME i1, SOME i2) => 984 and (k2,v2) = readIterator i2 990 and io2 = advanceIterator i2
|
/seL4-l4v-master/HOL4/examples/computability/kolmog/ |
H A D | plain_kolmog_inequalitiesScript.sml | 719 ������i2 b2. p2 = pair i2 b2��� 723 qabbrev_tac���ARG = pair (n2bl N1) (pair (n2bl SIb_i) (pair a1 (pair i1 b1) ++ pair i2 b2))��� >>
|