Searched refs:functions (Results 151 - 175 of 695) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A Dcompiler.sml46 (* Auxiliary functions. *)
57 (* Compiling a list of functions. *)
147 (* Compiling a list of source functions. *)
H A Dclosure.sml125 (* Move all functions definitions to top level *)
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A DregexpSyntax.sml81 (* The following commented out functions implement the maps for n-bit words *)
98 The following functions implement the maps for bool vectors
113 The following functions implement the maps for bool vectors
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DEncode.sml4 (* Derived from Konrad Slind's code to generate size functions *)
18 (* Helper functions. *)
148 (* 'a -> bool list variables : encode functions for type variables *)
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DconstrFamiliesLib.sig30 the main constructor functions + labelled args. *)
43 (* [make_constructorList exh constrs] is a convenience functions
138 This functions combines all the contents of a db to
H A DpatternMatchesLib.sig156 prove properties about functions defined
176 be handy, if the PMATCH contains functions
267 the guard is T. See below for functions using this
308 PMATCH_COMPLETE_CONV and similar functions instead
463 functions compute an implication, whose conclusion is the
486 The following functions try to compute the redundancy
529 functions.
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A Dpreface.tex37 explains the means by which meta-language functions can be used to
46 computable functions), which was intended for interactive automated reasoning
47 about higher order recursively defined functions. The interface of the logic
H A DQuantHeuristics.tex109 All these functions get a list of \emph{quantifier heuristic parameters} as arguments. These
292 user to provide a list of ML functions. These functions get the
297 p_b, p_c). P(p_a, p_b, p_c))\ p$ these functions are given the
309 list of functions to decide which variables to instantiate. However, this function is simpler, because it just needs
337 parameters that are explained below, these functions provide an
432 The function \holtxt{filter\_qp} allows to add ML-functions that filter the handled
433 quantifiers. These functions are given a variable $x$ and a term $P(x)$.
434 The tool only tries to instantiate $x$ in $P(x)$, if all filter functions
531 At the lowest level, the tool searches guesses using ML-functions
[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DSubst.sml189 val functions = value
191 fun add (_,t,s) = NameAritySet.union s (Term.functions t)
217 | matchList _ _ = raise Error "Subst.match: functions can't match vars";
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DSubst.sml189 val functions = value
191 fun add (_,t,s) = NameAritySet.union s (Term.functions t)
217 | matchList _ _ = raise Error "Subst.match: functions can't match vars";
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Dsets.tex427 \index{functions|(}%
429 functions. Some of the more important theorems are given along with the
436 Two functions are \textbf{equal}\indexbold{equality!of functions}
439 \textbf{extensionality}\indexbold{extensionality!for functions} for
440 functions:
468 \textbf{composition}\indexbold{composition!of functions} are
504 functions are total; in some cases, a function's natural domain is a subset
545 with, we need a law that relates the equality of functions to
553 extensionality.\indexbold{extensionality!for functions}
[all...]
H A Dbasics.tex51 \textbf{theory} is a named collection of types, functions, and theorems,
65 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
124 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
154 applying functions to arguments. If \isa{f} is a function of type
157 infix functions like \isa{+} and some basic constructs from functional
219 involving overloaded functions such as~\isa{+},
231 Isabelle allows infix functions like \isa{+}. The prefix form of function
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Dsets.tex427 \index{functions|(}%
429 functions. Some of the more important theorems are given along with the
436 Two functions are \textbf{equal}\indexbold{equality!of functions}
439 \textbf{extensionality}\indexbold{extensionality!for functions} for
440 functions:
468 \textbf{composition}\indexbold{composition!of functions} are
504 functions are total; in some cases, a function's natural domain is a subset
545 with, we need a law that relates the equality of functions to
553 extensionality.\indexbold{extensionality!for functions}
[all...]
H A Dbasics.tex51 \textbf{theory} is a named collection of types, functions, and theorems,
65 (types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
124 In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
154 applying functions to arguments. If \isa{f} is a function of type
157 infix functions like \isa{+} and some basic constructs from functional
219 involving overloaded functions such as~\isa{+},
231 Isabelle allows infix functions like \isa{+}. The prefix form of function
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DQuantHeuristics.tex109 All these functions get a list of \emph{quantifier heuristic parameters} as arguments. These
282 user to provide a list of ML functions. These functions get the
287 p_b, p_c). P(p_a, p_b, p_c))\ p$ these functions are given the
299 list of functions to decide which variables to instantiate. However, this function is simpler, because it just needs
327 parameters that are explained below, these functions provide an
422 The function \holtxt{filter\_qp} allows to add ML-functions that filter the handled
423 quantifiers. These functions are given a variable $x$ and a term $P(x)$.
424 The tool only tries to instantiate $x$ in $P(x)$, if all filter functions
521 At the lowest level, the tool searches guesses using ML-functions
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DpolytypicLib.sml10 (* Error handling functions: *)
156 (* Holds the theorems necessary for the creation of polytypic functions *)
160 (* functions, theorems : *)
161 (* Binary maps from types to strings to functions or theorems *)
163 (* The map from types to translating functions and theorems *)
172 type functions = (hol_type,(string,function) dict ref) dict; type
174 type translations = (hol_type,((functions ref * theorems ref) * translation_scheme)) dict;
196 (* Input testing functions: *)
230 (* Prints a list or a pair of items using supplied printing functions *)
247 (* General list processing functions *)
2823 val functions = map (get_def ## map get_def o fst) base_types handle e => wrap "" e value
3138 let val functions = flatten (map (map (CONV_RULE conv o get_def) o fst o snd) value
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_OPTIMISER.sml106 functions for each application. *)
246 (* When transforming code we only process one level and do not descend into sub-functions. *)
319 inline which is important if they are functions. The canonical
639 and repack argument functions.
860 (* Return the pair of functions. *)
941 (* Transforming a lambda may result in producing auxiliary functions that are in
960 (* Turn any bindings into extra mutually-recursive functions. *)
1046 2. Don't attempt to optimise inline functions that are exported.
1357 (* Once all the inlining is done we look for functions that can be compiled immediately.
1358 These are either functions wit
[all...]
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPmatchHeuristics.sml38 (* A heuristic based on ranking functions *)
70 (* ranking functions *)
121 (* heuristics defined using ranking functions *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dfile_readerLib.sml106 (* helper functions *)
216 val _ = f (" Total: " ^ names_count ^ " functions, " ^ inst_count ^
233 " functions ("
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/
H A Dexor32.ml55 (* These functions are added to a couple of global lists. *)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A Dord-map-sig.sml8 * Extended by two functions "update" and "findSome" - Martin Erwig
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A Dord-map-sig.sml8 * Extended by two functions "update" and "findSome" - Martin Erwig
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/
H A Dord-map-sig.sml8 * Extended by two functions "update" and "findSome" - Martin Erwig
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DStream.sml12 (* Helper functions. *)
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/MISC/
H A Deval-test.ml1 % File for testing the Lisp functions defined in hol/lisp/eval.l

Completed in 309 milliseconds

1234567891011>>