| /seL4-l4v-10.1.1/HOL4/src/portableML/mosml/concurrent/ |
| H A D | Sref.sig | 5 val new : 'a -> 'a t value
|
| H A D | Sref.sml | 8 fun new v = ref v function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/ |
| H A D | Sref.sig | 5 val new : 'a -> 'a t value
|
| H A D | Sref.sml | 6 fun new v = {mutex = Mutex.mutex(), v = ref v} function
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | ThyDataSexp.sig | 20 Thus, if the theory data is a list of values, both old and new should be
25 new data (representing a single key-value maplet) should be a singleton
28 val alist_merge : {old: t, new : t} -> t
29 val append_merge : {old : t, new : t} -> t
31 val new : {thydataty : string, value
32 merge : {old : t, new : t} -> t,
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
| H A D | MB_Monitor.sig | 4 val new : {info : string -> unit, value
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
| H A D | parser.h | 39 return strcpy(new char[strlen(s)+1], s);
|
| /seL4-l4v-10.1.1/l4v/tools/autocorres/experiments/alloc-proof/ |
| H A D | alloc_lite.c | 114 /* If we have space after the allocation, create a new node
166 struct mem_node *new = (struct mem_node *)ptr; local
174 /* Determine if we should merge with previous, or add a new node. */
175 if ((word_t)prev + prev->size == (word_t)new) {
177 new = prev;
179 new->size = size;
180 prev->next = new;
183 /* Determine if we should merge the next with the new. */
184 if ((word_t)new + new
[all...] |
| /seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/ |
| H A D | alloc.c | 98 /* If we have space after the allocation, create a new node
137 struct mem_node *new = (struct mem_node *)ptr; local
148 /* Determine if we should merge with previous, or add a new node. */
149 if ((word_t)prev + prev->size == (word_t)new) {
151 new = prev;
153 new->size = size;
154 prev->next = new;
157 /* Determine if we should merge the next with the new. */
158 if ((word_t)new + new
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | tailbuffer.sig | 5 val new : {numlines : int, patterns : string list} -> t value
|
| H A D | SourceFile.sig | 20 val new: string -> t value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
| H A D | quotient.sig | 24 (* an equivalence relation on the type, and creates a new type which *)
26 (* In addition to creating the new type, functions are defined in the *)
27 (* HOL logic to translate between the old and new types in both *)
52 string -> (* name of new quotient type *)
53 string -> (* name of abstraction function from old to new *)
54 string -> (* name of representation function from new to old *)
224 fname : string, (* name of new function *)
226 fixity : Parse.fixity option} -> (* fixity of new function *)
227 Thm.thm (* definition of a new lifted function *)
248 Thm.thm list -> (* new functio
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | AtomNet.sml | 32 val new = TermNet.new; value
38 fun fromList parm l = List.foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
|
| H A D | Active.sig | 36 (* Create a new active clause set and initialize clauses. *)
39 val new : value
|
| H A D | Heap.sig | 11 val new : ('a * 'a -> order) -> 'a heap value
|
| H A D | LiteralNet.sml | 25 fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm}; function
42 fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
|
| H A D | Resolution.sml | 33 fun new parameters ths = function
37 val (active,cls) = Active.new activeParm ths (* cls = factored ths *)
39 val waiting = Waiting.new waitingParm cls
46 val () = Print.trace Print.ppException "Resolution.new: exception" e
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | AtomNet.sml | 32 val new = TermNet.new; value
38 fun fromList parm l = List.foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
|
| H A D | Active.sig | 36 (* Create a new active clause set and initialize clauses. *)
39 val new : value
|
| H A D | Heap.sig | 11 val new : ('a * 'a -> order) -> 'a heap value
|
| H A D | LiteralNet.sml | 25 fun new parm = {positive = AtomNet.new parm, negative = AtomNet.new parm}; function
42 fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
|
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttRedirect.sml | 32 push_out_file: start a new output file, stacking the file descriptor.
40 (dup2{old = fd, new = stdout}; stack := fd :: !stack)
59 fd :: _ => (dup2{old = fd, new = stdout}; true)
60 | [] => (dup2{old = duplicate_stdout, new = stdout}; false))
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibSupport.sig | 35 val new : parameters -> formula list -> clause list -> sos value
40 (* Adding new clauses *)
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibAbbrev.sig | 9 (* introduce a new variable as abbreviation for terms selected by the selection_funs
14 (* a simple version that does not try to instantiate the new quatifier *)
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | GrammarAncestry.sml | 11 Theory.LoadableThyData.new {thydataty = tag, merge = op @,
|