/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Heap.h | 34 C comp; member in class:Heap 41 while (parent(i) != 0 && comp(x,heap[parent(i)])){ 54 int child = right(i) < heap.size() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i); 55 if (!comp(heap[child],x)) break; 67 Heap(C c) : comp(c) { heap.push(-1); } 95 || ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
|
/seL4-l4v-master/HOL4/src/0/ |
H A D | Subst.sig | 11 val comp : ('a subs * 'a -> 'a) -> 'a subs * 'a subs -> 'a subs value
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Printbase.sml | 13 fun prentry {comp, file, line} = 19 case comp of 54 | nextstr last ((e1 as {comp, file, ...}) :: erest) = 55 if comp = last then 59 and newitem (e1 as {comp, file, ...}) erest = 64 out (case comp of 72 nextstr comp erest)
|
H A D | Parsspec.sml | 30 {comp = Val (getId idInfo), file = str, line = #2 pos1} :: res 32 {comp = Val (getId idInfo), file = str, line = #2 pos1} :: res 34 {comp = Typ (getId idInfo), file = str, line = #2 pos1} :: res 36 {comp = Typ (getId idInfo), file = str, line = #2 pos1} :: res 38 {comp = Con (getId idInfo), file = str, line = #2 pos1} :: res 40 {comp = Typ (getId idInfo), file = str, line = #2 pos1} 43 {comp = Typ (getId idInfo), file = str, line = #2 pos1} :: res 45 {comp = Exc (getId idInfo), file = str, line = #2 pos1} :: res 75 val initialbase = {comp = Database.Str, file = str, line = 0} :: res
|
H A D | Htmlsigs.sml | 67 fun comp2str comp = 70 case comp of 109 List.map #comp (List.filter relevant (lookup (db, id))) 111 fun indexcomp comp = 112 case comp of 113 Exc i => if i=id then SOME comp else NONE 114 | Typ i => if i=id andalso linehas "type" then SOME comp 116 | Con i => if i=id then SOME comp else NONE 117 | Val i => if i=id then SOME comp else NONE 118 | Str => if linehas "structure" then SOME comp [all...] |
H A D | MyDatabase.sml | 16 type entry = { comp : component, file : string, line : int } 81 fun getname ({comp, file, ...} : entry) = 82 case comp of
|
H A D | Database.sig | 13 type entry = { comp : component, file : string, line : int }
|
H A D | MyDatabase-sig.sml | 16 type entry = { comp : component, file : string, line : int }
|
H A D | Database.sml | 117 type entry = { comp : component, file : string, line : int } 120 (writeComponent os (#comp e); 130 {comp = c, file = f, line = l} 214 fun getname ({comp, file, ...} : entry) = 215 case comp of
|
/seL4-l4v-master/isabelle/lib/browser/awtUtilities/ |
H A D | Border.java | 19 public Border(Component comp,int s) { argument 21 add(comp);
|
/seL4-l4v-master/l4v/isabelle/lib/browser/awtUtilities/ |
H A D | Border.java | 19 public Border(Component comp,int s) { argument 21 add(comp);
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | protocol.tex | 9 \def\comp#1{\lbb#1\rbb} 58 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ 59 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ 60 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} 72 $\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what 85 &1.&\quad A\to C &: \comp{Na,A}\sb{Kc} && 86 \qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ 87 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ 88 &3.&\quad A\to C &: \comp{Nb}\sb{Kc} && 89 \qquad 3'.&\quad C\to B &: \comp{N [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | protocol.tex | 9 \def\comp#1{\lbb#1\rbb} 58 &1.&\quad A\to B &: \comp{Na,A}\sb{Kb} \\ 59 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ 60 &3.&\quad A\to B &: \comp{Nb}\sb{Kb} 72 $\comp{Na,A}\sb{Kb}$ and extracted~$Na$. That is precisely what 85 &1.&\quad A\to C &: \comp{Na,A}\sb{Kc} && 86 \qquad 1'.&\quad C\to B &: \comp{Na,A}\sb{Kb} \\ 87 &2.&\quad B\to A &: \comp{Na,Nb}\sb{Ka} \\ 88 &3.&\quad A\to C &: \comp{Nb}\sb{Kc} && 89 \qquad 3'.&\quad C\to B &: \comp{N [all...] |
/seL4-l4v-master/l4v/tools/c-parser/standalone-parser/ |
H A D | basics.sml | 20 let fun comp ([],[]) = EQUAL function 21 | comp ([], _) = LESS 22 | comp (_, []) = GREATER 23 | comp (h1::t1, h2::t2) = 24 case cfn (h1,h2) of EQUAL => comp (t1,t2) | x => x 25 in comp end;
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | totoScript.sml | 74 val _ = type_abbrev ("comp", Type`:'a->'a->cpn`); 76 val TotOrd = Define`TotOrd (c: 'a comp) = 115 val TO_exists = maybe_thm ("TO_exists", Term`?x:'a comp. TotOrd x`, 123 |- ?(rep :'x toto -> 'x comp). TYPE_DEFINITION (TotOrd :'x comp -> bool) rep*) 136 TO_apto_TO_ID = |- !(r :'x comp). TotOrd r <=> (apto (TO r) = r) *) 140 (* TO_11 = |- !(r :'x comp) (r' :'x comp). 145 (* onto_apto = |- !(r :'x comp). TotOrd r <=> ?(a :'x toto). r = apto a *) 149 (* TO_onto = |- !(a :'x toto). ?(r :'x comp) [all...] |
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | inference_rulesScript.sml | 370 Define `preserve_relation_mmu comp invr1 invr2 f y = 378 ((?a s1' s2'.((comp s1 = ValueState a s1') /\ (comp s2 = ValueState a s2') /\ 387 \/ (? e. (comp s1 = Error e) /\ (comp s2 = Error e)))`; 391 val preserve_relation_mmu_abs_def = Define `preserve_relation_mmu_abs comp invr1 invr2 f y = 399 ((?a s1' s2'.((comp c s1 = ValueState a s1') /\ (comp c s2 = ValueState a s2') /\ 408 \/ (? e. (comp c s1 = Error e) /\ (comp [all...] |
H A D | ARM_prover_toolsLib.sml | 100 val (rel, comp) = dest_comb rc 101 val (thm, _) = prove_it comp i1 i2 unt simp 185 COMB (rel, comp) => 206 COMB (rel, comp) => if (i2 ~~ ``little_mode_mix:(arm_state->bool)``)
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | symbols_dockable.scala | 192 val comp = group_tabs.peer 193 GUI.traverse_components(comp, 203 comp.revalidate 204 comp.repaint()
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | symbols_dockable.scala | 192 val comp = group_tabs.peer 193 GUI.traverse_components(comp, 203 comp.revalidate 204 comp.repaint()
|
/seL4-l4v-master/HOL4/examples/elliptic/swsep/ |
H A D | examples.sml | 28 val comp = pp_compile def prove_equiv; value 30 val spec = spec_sep comp
|
H A D | swsepLib.sml | 52 fun spec_ir comp = 54 val (spec, wf, ir) = extract_ir comp; 149 fun spec_sep (comp:(string * hol_type * (IRSyntax.exp * 'a * IRSyntax.exp) * thm list * thm * thm * thm * thm * thm * string * string list)) = 151 val (spec, wf, ir) = extract_ir comp; 152 val input_regs = listSyntax.mk_list (map IRSyntax.convert_reg (IRSyntax.pair2list (#1 (#3 comp))), Type `:MREG`); 154 val unchanged_thm = CONJUNCT1 (REWRITE_RULE [ILTheory.UNCHANGED_STACK_def] (#9 comp))
|
/seL4-l4v-master/isabelle/src/Pure/GUI/ |
H A D | gui.scala | 197 def traverse(comp: Component) 199 apply(comp) 200 comp match {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/GUI/ |
H A D | gui.scala | 197 def traverse(comp: Component) 199 apply(comp) 200 comp match {
|
/seL4-l4v-master/HOL4/examples/category/ |
H A D | categoryScript.sml | 73 comp : (��,��) mor -> (��,��) mor -> �� |>`; 144 compose_in c = CURRY (restrict (UNCURRY (compose c.comp)) {(f,g) | f ���> g -: c})`; 150 `���c f g. f ���> g -:c ��� (g o f -: c = compose c.comp f g)`, 156 extensional (UNCURRY c.comp) {(f,g) | f ���> g -: c} 188 comp := CURRY (restrict (UNCURRY c.comp) {(f,g) | f ���> g -: c}) |>`; 727 unit_cat = mk_cat <| obj := {()}; mor := {ARB:(unit,unit) mor}; id_map := ARB; comp := ARB |>`; 775 id_map := K (); comp := K (K ()) |>`; 839 comp := K (K ()) |>`; 942 id_map := c.id_map; comp [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | compiler.sml | 61 fun compenv comp = 67 case total comp (env,h) 151 fun compenv comp = 157 case total comp (env,h)
|