/seL4-l4v-10.1.1/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...] |
H A D | description.tex | 5 the pair library, hereafter referred to as `the Software'. 36 \chapter{The pair Library} 38 This manual describes the use of the pair library. 39 The pair library has been provided to reduce the difficulty of reasoning 41 The pair library contains a version of every standard \HOL\ function 44 pair library provides paired equivalents: 169 The pair library also contains many functions for which there are no 175 you must load the pair library. 176 To load the pair library, issue the following command: 178 load_library `pair`;; [all...] |
/seL4-l4v-10.1.1/graph-refine/ |
H A D | graph-refine.py | 35 def toplevel_check (pair, check_loops = True, report = False, count = None, 38 printout ('Testing Function pair %s' % pair) 43 for (tag, fname) in pair.funs.iteritems (): 45 printout ('Skipping %s, underspecified %s' % (pair, tag)) 57 p = check.build_problem (pair) 101 trace ('EXCEPTION in handling %s:' % pair) 113 printout ('Result %s for pair %s, time taken: %.2fs' 114 % (result, pair, end_time - start_time)) 124 pairs = list (set ([pair fo [all...] |
H A D | stats.py | 17 pairings_names = dict ([(pair.name, pair) for pair in pairings_set]) 20 (_, nm) = line.split (' pair ', 1) 22 pair = pairings_names[nm] 25 proofs[pair] = pn 31 for (pair, proof) in proofs.iteritems (): 36 p = check.build_problem (pair) 142 print 'Search pair decay in random examples (idx, window size, trace):' 146 print 'Search pair deca [all...] |
/seL4-l4v-10.1.1/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-10.1.1/graph-refine/example/ |
H A D | target.py | 36 pair = logic.mk_pairing (functions, f, f2) 37 pairings[f] = [pair] 38 pairings[f2] = [pair]
|
/seL4-l4v-10.1.1/graph-refine/loop-example/synth/ |
H A D | target.py | 36 pair = logic.mk_pairing (functions, f, f2) 37 pairings[f] = [pair] 38 pairings[f2] = [pair]
|
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/isabelle/src/Pure/ |
H A D | term_xml.scala | 32 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, 33 { case App(a, b) => (Nil, pair(term, term)(a, b)) })) 54 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, 55 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/ |
H A D | term_xml.scala | 32 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, 33 { case App(a, b) => (Nil, pair(term, term)(a, b)) })) 54 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, 55 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | realLib.sig | 14 (* Incorporates simpsets for bool, pair, and arithmetic *)
|
/seL4-l4v-10.1.1/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-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | protocol.scala | 19 Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text))) 370 Symbol.encode_yxml(list(pair(string, string))(table)) 382 Symbol.encode_yxml(list(pair(string, properties))(lst)) 410 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, 413 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) 420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) 451 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, 458 pair(string, pair(strin [all...] |
H A D | command.scala | 39 { import XML.Encode._; list(pair(long, tree))(results.rep.toList) } 42 { import XML.Decode._; make(list(pair(long, tree))(body)) } 126 pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name) 131 list(pair(markup_index, markup_tree))(markups.rep.toList) 140 val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body) 144 (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _) 236 pair(long, pair(string, pair(pair(lis [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | protocol.scala | 19 Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text))) 370 Symbol.encode_yxml(list(pair(string, string))(table)) 382 Symbol.encode_yxml(list(pair(string, properties))(lst)) 410 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, 413 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) 420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) 451 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, 458 pair(string, pair(strin [all...] |
H A D | command.scala | 39 { import XML.Encode._; list(pair(long, tree))(results.rep.toList) } 42 { import XML.Decode._; make(list(pair(long, tree))(body)) } 126 pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name) 131 list(pair(markup_index, markup_tree))(markups.rep.toList) 140 val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body) 144 (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _) 236 pair(long, pair(string, pair(pair(lis [all...] |
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | graph_display.scala | 61 list(pair(pair(string, pair(string, x => x)), list(string)))(body)
|
/seL4-l4v-10.1.1/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-10.1.1/isabelle/src/Pure/Tools/ |
H A D | print_operation.scala | 35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
|
H A D | build.scala | 219 pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool, 220 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, 221 pair(strin [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | print_operation.scala | 35 list(pair(string, string))(Symbol.decode_yxml(msg.text))
|
/seL4-l4v-10.1.1/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
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairSyntax.sml | 18 Type.mk_thy_type {Tyop = "prod", Thy = "pair", Args = [ty1, ty2]} 22 SOME{Tyop = "prod", Thy = "pair", Args = [ty1, ty2]} => (ty1, ty2) 35 val fst_tm = prim_mk_const {Name="FST", Thy="pair"} 36 val snd_tm = prim_mk_const {Name="SND", Thy="pair"} 37 val curry_tm = prim_mk_const {Name="CURRY", Thy="pair"} 38 val pair_map_tm = prim_mk_const {Name="##", Thy="pair"} 39 val lex_tm = prim_mk_const {Name="LEX", Thy="pair"} 40 val swap_tm = prim_mk_const {Name="SWAP", Thy="pair"} 41 val pair_case_tm = prim_mk_const {Name = "pair_CASE", Thy = "pair"} 44 Make a pair fro [all...] |