Searched refs:comp (Results 1 - 25 of 55) sorted by relevance

123

/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DHeap.h34 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 DSubst.sig11 val comp : ('a subs * 'a -> 'a) -> 'a subs * 'a subs -> 'a subs value
/seL4-l4v-master/HOL4/help/src-sml/
H A DPrintbase.sml13 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 DParsspec.sml30 {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 DHtmlsigs.sml67 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 DMyDatabase.sml16 type entry = { comp : component, file : string, line : int }
81 fun getname ({comp, file, ...} : entry) =
82 case comp of
H A DDatabase.sig13 type entry = { comp : component, file : string, line : int }
H A DMyDatabase-sig.sml16 type entry = { comp : component, file : string, line : int }
H A DDatabase.sml117 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 DBorder.java19 public Border(Component comp,int s) { argument
21 add(comp);
/seL4-l4v-master/l4v/isabelle/lib/browser/awtUtilities/
H A DBorder.java19 public Border(Component comp,int s) { argument
21 add(comp);
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dprotocol.tex9 \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 Dprotocol.tex9 \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 Dbasics.sml20 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 DtotoScript.sml74 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 Dinference_rulesScript.sml370 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 DARM_prover_toolsLib.sml100 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 Dsymbols_dockable.scala192 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 Dsymbols_dockable.scala192 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 Dexamples.sml28 val comp = pp_compile def prove_equiv; value
30 val spec = spec_sep comp
H A DswsepLib.sml52 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 Dgui.scala197 def traverse(comp: Component)
199 apply(comp)
200 comp match {
/seL4-l4v-master/l4v/isabelle/src/Pure/GUI/
H A Dgui.scala197 def traverse(comp: Component)
199 apply(comp)
200 comp match {
/seL4-l4v-master/HOL4/examples/category/
H A DcategoryScript.sml73 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 Dcompiler.sml61 fun compenv comp =
67 case total comp (env,h)
151 fun compenv comp =
157 case total comp (env,h)

Completed in 374 milliseconds

123