| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sig | 20 (* case expression manipulation functions *)
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Int_extra.sml | 3 (* DESCRIPTION : Additional functions for integer arithmetic in ML. *)
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | parse_type.sig | 27 (* The record of functions specify how to deal with the need to
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | UTF8Set.sig | 17 encoding) string is passed to any of these functions then the UTF8.BadUTF8
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | ThyDataSexp.sig | 19 (* note that merge functions must take identical "types" on both sides.
|
| /seL4-l4v-10.1.1/HOL4/src/string/ |
| H A D | ASCIInumbersSyntax.sml | 7 (* Helper functions *)
|
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttTimeout.sml | 3 (* DESCRIPTION : Timing out PolyML functions. *)
|
| /seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
| H A D | call_graph_utils.py | 15 #functions f called
87 def makeCallGraph(fun,functions,dir_name):
88 cg = funsCallGraph(functions,dir_name,[])
134 #dict of number of transitively called functions to caller functions
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | inductive0.tex | 5 recursive functions and datatypes: inductively defined sets.
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | inductive0.tex | 5 recursive functions and datatypes: inductively defined sets.
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | AtomNet.sml | 12 (* Helper functions. *)
|
| H A D | Model.sml | 18 (* Helper functions. *)
116 {functions : fixedFunction NameArityMap.map,
148 {functions = fns,
154 val Fixed {functions = fns, ...} = fix
178 val Fixed {functions = fns, relations = rels} = fix
183 {functions = fns,
189 val Fixed {functions = fns, relations = rels} = fix
194 {functions = fns,
203 val Fixed {functions = fns1, relations = rels1} = fix1
204 and Fixed {functions
[all...] |
| H A D | Term.sig | 51 val functions : term -> NameAritySet.set value
63 (* Binary functions *)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | AtomNet.sml | 12 (* Helper functions. *)
|
| H A D | Model.sml | 18 (* Helper functions. *)
116 {functions : fixedFunction NameArityMap.map,
148 {functions = fns,
154 val Fixed {functions = fns, ...} = fix
178 val Fixed {functions = fns, relations = rels} = fix
183 {functions = fns,
189 val Fixed {functions = fns, relations = rels} = fix
194 {functions = fns,
203 val Fixed {functions = fns1, relations = rels1} = fix1
204 and Fixed {functions
[all...] |
| H A D | Term.sig | 51 val functions : term -> NameAritySet.set value
63 (* Binary functions *)
|
| /seL4-l4v-10.1.1/HOL4/src/rational/ |
| H A D | jbUtils.sml | 5 * useful conversions, tactics, and ML functions
83 * ML functions
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | trace_refute.py | 20 from target_objects import functions, trace, pairings, symbols, printout namespace
81 for n in functions[f].nodes:
96 """get the fraction of instructions covered by some functions"""
105 of the number of instruction addresses, skipping functions
127 """mirrors build_problem from check for multiple functions"""
143 p.add_entry_function (functions[fname], tag)
225 inps = functions[fname].inputs
313 cn = find_actual_call_node (functions[prev_fn], call)
314 fn = functions[prev_fn].nodes[cn].fname
349 p = functions[
[all...] |
| H A D | stack_logic.py | 17 from target_objects import functions, trace, pairings, pre_pairings, printout namespace
251 """all functions will keep the stack pointer equal, whether they have
329 fun = functions[fname]
727 fun = functions[fname]
770 fun = functions[fname]
840 graph = dict ([(f, list (functions[f].function_calls ()))
841 for f in functions])
866 prevs = set ([f for f in functions
867 if [f2 for f2 in functions[f].function_calls () if f2 in group]])
884 p.add_entry_function (functions[
[all...] |
| H A D | target_objects.py | 25 functions = {} variable
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/equiv/ |
| H A D | EquivType.sml | 3 (* functions and theorems about the representatives over to the new type. *)
15 (* welldefs - theorems asserting that the old functions are welldefined; *)
21 (* thlist - List of theorems about the old functions *)
27 (* * All original functions must be curried (as are the new ones). *)
34 (* old functions become the new ones. *)
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/ |
| H A D | elsaUtils.sml | 3 (* functions.sml and before that, start_groups.ml) *)
4 (* DESCRIPTION : defines a collection of general purpose functions, *)
38 (* Some general-purpose functions *)
70 mapshape applies the functions in functions to argument lists obtained by
74 fun mapshape {partition = [],functions = [], unionlist = []} = []
76 functions = (f::rem_funs),
84 functions = rem_funs,
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
| H A D | modelCheckLib.sig | 14 All functions return a thm option. If the specific property can be
16 SOME thm. If it can not be proved these functions print out a
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Functions/document/ |
| H A D | intro.tex | 11 defining functions quickly. For the more difficult definitions we will
55 and tail recursive functions.
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Functions/document/ |
| H A D | intro.tex | 11 defining functions quickly. For the more difficult definitions we will
55 and tail recursive functions.
|