| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | satCommonTools.sml | 33 let val ins = TextIO.openIn (fname^".term") value
|
| H A D | satTools.sml | 81 val ins = TextIO.openIn outfile value
|
| H A D | dimacsTools.sml | 373 val ins = TextIO.openIn fullfilename value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibPatricia.sml | 73 fun ins t = function
|
| H A D | mlibResolution.sml | 71 local fun ins (c,i) = Intmap.insert (i, #id (mlibClause.dest_clause c), c); function
|
| H A D | mlibTermnet.sml | 143 fun ins a tm (i,n) = SOME (i + 1, oadd (RESULT [a]) [tm] n); function
|
| H A D | mlibThm.sml | 235 fun ins (th,a) m = Binarymap.insert (m,th,a); function
257 fun ins f th (s,a) = (Binaryset.add (s,th), f (th,a)) function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | PIntMap.sml | 79 fun ins t = function
|
| H A D | Redblackmap.sml | 54 fun ins LEAF = RED(key,data NONE,LEAF,LEAF) function
|
| H A D | Redblackset.sml | 57 fun ins LEAF = (RED(elm,LEAF,LEAF), 1) function
|
| /seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
| H A D | Binarymap.sml | 144 let fun ins E = T{key=x,value=v,cnt=1,left=E,right=E} function
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | codegen_armLib.sml | 30 fun ins [] = [] function
|
| /seL4-l4v-10.1.1/HOL4/developers/mlton-srcs/ |
| H A D | Binarymap.sml | 213 let fun ins E = T{key=x,value=v,cnt=1,left=E,right=E} function
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | int-binary-map.sml | 277 fun ins (key, x, m) = (case find(m, key) function
287 fun ins (key, x, m) = (case find(m, key) function
300 fun ins (key, x, m) = (case find(m2, key) function
316 fun ins (key, x, m) = (case find(m2, key) function
[all...] |
| H A D | IRSyntax.sml | 395 val (ins, temps, outs) = (filter_inputs INPUT, filter_out_stack INSTACK, filter_out_stack OUTPUT); value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | int-binary-map.sml | 277 fun ins (key, x, m) = (case find(m, key) function
287 fun ins (key, x, m) = (case find(m, key) function
300 fun ins (key, x, m) = (case find(m2, key) function
316 fun ins (key, x, m) = (case find(m2, key) function
[all...] |
| H A D | IRSyntax.sml | 387 val (ins, temps, outs) = (filter_inputs INPUT, filter_out_stack INSTACK, filter_out_stack OUTPUT); value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
| H A D | int-binary-map.sml | 277 fun ins (key, x, m) = (case find(m, key) function
287 fun ins (key, x, m) = (case find(m, key) function
300 fun ins (key, x, m) = (case find(m2, key) function
316 fun ins (key, x, m) = (case find(m2, key) function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
| H A D | Opentheory.sml | 73 fun ins (th,n) = Net.insert (concl th,th) n function
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/ |
| H A D | testEncode.sml | 547 val ins = value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | IRSyntax.sml | 387 val (ins, temps, outs) = (filter_inputs INPUT, filter_out_stack INSTACK, filter_out_stack OUTPUT); value
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake_types.sml | 337 fun ins (k,v) env = Binarymap.insert(env,k,v) function
|
| H A D | internal_functions.sml | 284 val ins = textInstreamOf proc value
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | TermNet.sml | 184 fun ins a qtm (i,n) = SOME (i + 1, oadd (Result [a]) [qtm] n); function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | TermNet.sml | 184 fun ins a qtm (i,n) = SOME (i + 1, oadd (Result [a]) [qtm] n); function
|