/seL4-l4v-master/HOL4/src/coretypes/pair-Manual/ |
H A D | Makefile | 2 # 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 D | graph-refine.py | 33 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 D | stats.py | 23 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 D | ILTheory.sml | 23 ((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 D | plain_kolmog_inequalitiesScript.sml | 19 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 D | kolmog_inequalitiesScript.sml | 18 (* 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 D | target.py | 34 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 D | target.py | 34 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 D | pairs.c | 137 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 D | term_xml.scala | 38 { 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 D | term_xml.scala | 38 { 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 D | export_theory.scala | 280 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 D | export_theory.scala | 280 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 D | ml_syntax.scala | 49 /* 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 D | ml_syntax.scala | 49 /* 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 D | realLib.sig | 14 (* Incorporates simpsets for bool, pair, and arithmetic *)
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/solitare/ |
H A D | solitare.cxx | 19 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 D | protocol.scala | 233 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 D | protocol.scala | 233 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 D | graph_display.scala | 61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | graph_display.scala | 61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | print_operation.scala | 35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | print_operation.scala | 35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | pairSimps.sml | 7 val PAIR_ss = BasicProvers.thy_ssfrag "pair"
|
/seL4-l4v-master/HOL4/src/0/ |
H A D | KernelTypes.sml | 5 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
|