Searched refs:pair (Results 1 - 25 of 334) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/coretypes/pair-Manual/
H A DMakefile2 # Make the manual for the "pair" library #
30 entries.tex theorems.tex *.ind pair.ps pair.pdf
36 echo "\chapter{ML Functions in the pair Library}" >entries.tex; \
47 ${MAKEINDEX} pair.idx
49 pair:
50 latex pair.tex
53 dvips pair.dvi -o
55 pdf: pair.ps
56 pdflatex pair
[all...]
/seL4-l4v-master/graph-refine/
H A Dgraph-refine.py33 def toplevel_check (pair, check_loops = True, report = False, count = None,
36 printout ('Testing Function pair %s' % pair)
41 for (tag, fname) in pair.funs.iteritems ():
43 printout ('Skipping %s, underspecified %s' % (pair, tag))
55 p = check.build_problem (pair)
99 trace ('EXCEPTION in handling %s:' % pair)
111 printout ('Result %s for pair %s, time taken: %.2fs'
112 % (result, pair, end_time - start_time))
122 pairs = list (set ([pair fo
[all...]
H A Dstats.py23 pairings_names = dict ([(pair.name, pair) for pair in pairings_set])
26 (_, nm) = line.split (' pair ', 1)
28 pair = pairings_names[nm]
31 proofs[pair] = pn
37 for (pair, proof) in proofs.iteritems ():
42 p = check.build_problem (pair)
148 print 'Search pair decay in random examples (idx, window size, trace):'
152 print 'Search pair deca
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DILTheory.sml23 ((T"prod" "pair"
24 [T"MREG" "IL" [], T"prod" "pair" [alpha, T"MEXP" "IL" []]] -->
25 T"prod" "pair"
27 T"prod" "pair" [alpha, T"EXP" "preARM" []]]))),
32 [T"prod" "pair"
34 T"prod" "pair"
35 [T"prod" "pair" [T"num" "num" [], T"OFFSET" "preARM" []],
36 T"prod" "pair"
38 T"prod" "pair"
40 T"prod" "pair"
[all...]
/seL4-l4v-master/HOL4/examples/computability/kolmog/
H A Dplain_kolmog_inequalitiesScript.sml19 U (pair x (pair i y)) =
20 on2bl (Phi (bl2n i) (bl2n (pair x y)))) ���
21 ���m. (���i x y. m <> pair x (pair i y)) ==> U m = NONE
33 qexists_tac ���pair x (pair (n2bl i) [])��� >>
47 univ_plmach U ��� {p | U (pair y p) = SOME x} ��� ���
52 ������i b c. a = pair b (pair
[all...]
H A Dkolmog_inequalitiesScript.sml18 (* rename pair to bl pair etc *)
23 U (pair x (pair i y)) =
24 on2bl (Phi Upfi (bl2n i ��� bl2n (pair x y)))) ���
25 ���m. (���i x y. m <> pair x (pair i y)) ==> U m = NONE
45 ���(���x y z. a1 = pair x (pair y z)) ���
46 (���u v w. a2 = pair
[all...]
/seL4-l4v-master/graph-refine/example/
H A Dtarget.py34 pair = logic.mk_pairing (functions, f, f2)
35 pairings[f] = [pair]
36 pairings[f2] = [pair]
/seL4-l4v-master/graph-refine/loop-example/synth/
H A Dtarget.py34 pair = logic.mk_pairing (functions, f, f2)
35 pairings[f] = [pair]
36 pairings[f2] = [pair]
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/
H A Dpairs.c137 SHORT {* creates an empty variable pair table *}
178 SHORT {* set one variable pair *}
179 PROTO {* int bdd_setpair(bddPair *pair, int oldvar, int newvar)
180 int bdd_setbddpair(bddPair *pair, BDD oldvar, BDD newvar) *}
181 DESCR {* Adds the pair {\tt (oldvar,newvar)} to the table of pairs
182 {\tt pair}. This results in {\tt oldvar} being substituted
195 int bdd_setpair(bddPair *pair, int oldvar, int newvar) argument
197 if (pair == NULL)
205 bdd_delref( pair->result[bddvar2level[oldvar]] );
206 pair
216 bdd_setbddpair(bddPair *pair, int oldvar, BDD newvar) argument
251 bdd_setpairs(bddPair *pair, int *oldvar, int *newvar, int size) argument
265 bdd_setbddpairs(bddPair *pair, int *oldvar, BDD *newvar, int size) argument
[all...]
/seL4-l4v-master/isabelle/src/Pure/
H A Dterm_xml.scala38 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
39 { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
66 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
67 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
80 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
81 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
92 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
93 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
94 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
95 { case (Nil, a) => val (b, c) = pair(proo
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/
H A Dterm_xml.scala38 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
39 { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
66 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
67 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
80 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
81 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
92 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
93 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
94 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
95 { case (Nil, a) => val (b, c) = pair(proo
[all...]
/seL4-l4v-master/isabelle/src/Pure/Thy/
H A Dexport_theory.scala280 pair(decode_syntax,
281 pair(list(string),
282 pair(Term_XML.Decode.typ,
283 pair(option(Term_XML.Decode.term), bool))))(body)
309 triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
389 pair(list(pair(string, sort)), pair(list(pair(strin
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/
H A Dexport_theory.scala280 pair(decode_syntax,
281 pair(list(string),
282 pair(Term_XML.Decode.typ,
283 pair(option(Term_XML.Decode.term), bool))))(body)
309 triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
389 pair(list(pair(string, sort)), pair(list(pair(strin
[all...]
/seL4-l4v-master/isabelle/src/Pure/ML/
H A Dml_syntax.scala49 /* pair */
51 def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
52 "(" + f(pair._1) + ", " + g(pair._2) + ")"
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/
H A Dml_syntax.scala49 /* pair */
51 def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
52 "(" + f(pair._1) + ", " + g(pair._2) + ")"
/seL4-l4v-master/HOL4/src/real/
H A DrealLib.sig14 (* Incorporates simpsets for bool, pair, and arithmetic *)
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/solitare/
H A Dsolitare.cxx19 bddPair *pair; // Renaming pair variable
130 // Make renaming pair and current state variables
133 pair = bdd_newpair();
135 bdd_setpair(pair, n*2+1, n*2);
156 next = bdd_replace(next, pair);
181 next = bdd_replace(next, pair);
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dprotocol.scala233 Symbol.encode_yxml(list(pair(string, string))(table))
245 Symbol.encode_yxml(list(pair(string, properties))(lst))
273 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
276 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
281 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
304 pair(string, pair(string, pair(string, pair(string, list(string)))))(
348 { case Document.Node.Edits(a) => (Nil, list(pair(optio
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/
H A Dprotocol.scala233 Symbol.encode_yxml(list(pair(string, string))(table))
245 Symbol.encode_yxml(list(pair(string, properties))(lst))
273 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
276 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
281 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
304 pair(string, pair(string, pair(string, pair(string, list(string)))))(
348 { case Document.Node.Edits(a) => (Nil, list(pair(optio
[all...]
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dgraph_display.scala61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dgraph_display.scala61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dprint_operation.scala35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dprint_operation.scala35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
/seL4-l4v-master/HOL4/src/coretypes/
H A DpairSimps.sml7 val PAIR_ss = BasicProvers.thy_ssfrag "pair"
/seL4-l4v-master/HOL4/src/0/
H A DKernelTypes.sml5 Elements in signatures are determined by a (name,theory) pair.
7 create more than one such pair, and they need to be distinguished).
47 The representation of theorems. A "tag" is a pair of the oracles

Completed in 232 milliseconds

1234567891011>>