| /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
|
| H A D | Rewrite.sml | 181 fun ins redexes redex id ort = TermNet.insert redexes (redex,(id,ort)); function
|
| H A D | Map.sml | 1091 fun ins (key_value,acc) = insert acc key_value function
|
| H A D | KeyMap.sml | 1099 fun ins (key_value,acc) = insert acc key_value 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
|
| H A D | Rewrite.sml | 181 fun ins redexes redex id ort = TermNet.insert redexes (redex,(id,ort)); function
|
| H A D | Map.sml | 1091 fun ins (key_value,acc) = insert acc key_value function
|
| H A D | KeyMap.sml | 1099 fun ins (key_value,acc) = insert acc key_value function
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | internal_functions.sml | 284 val ins = textInstreamOf proc value
|
| H A D | Holmake_types.sml | 337 fun ins (k,v) env = Binarymap.insert(env,k,v) 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/src/pred_set/src/ |
| H A D | PFset_conv.sml | 215 val ins = (rator o rand) rhs value
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | Theory.sml | 205 fun ins (a::rst) = if same a then addp a::rst else a::ins rst function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | Redblackset.sml | 57 fun ins LEAF = (RED(elm,LEAF,LEAF), 1) function
|
| H A D | Redblackmap.sml | 54 fun ins LEAF = RED(key,data NONE,LEAF,LEAF) function
|
| H A D | PIntMap.sml | 79 fun ins t = function
|
| /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/src/metis/ |
| 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
|
| H A D | mlibTermnet.sml | 143 fun ins a tm (i,n) = SOME (i + 1, oadd (RESULT [a]) [tm] n); 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 | mlibPatricia.sml | 73 fun ins t = function
|
| H A D | mlibClauseset.sml | 540 fun ins (parm : parameters) cl (cls,set,subs) = function
|
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | PairRules.sml | 2407 val ins = match_term con gl value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | satTools.sml | 81 val ins = TextIO.openIn outfile value
|
| H A D | satCommonTools.sml | 33 let val ins = TextIO.openIn (fname^".term") value
|