/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | compiler.sml | 46 (* Auxiliary functions. *) 57 (* Compiling a list of functions. *) 147 (* Compiling a list of source functions. *)
|
H A D | closure.sml | 125 (* Move all functions definitions to top level *)
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | regexpSyntax.sml | 81 (* 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 D | Encode.sml | 4 (* 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 D | constrFamiliesLib.sig | 30 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 D | patternMatchesLib.sig | 156 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 D | preface.tex | 37 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 D | QuantHeuristics.tex | 109 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 D | Subst.sml | 189 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 D | Subst.sml | 189 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 D | sets.tex | 427 \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 D | basics.tex | 51 \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 D | sets.tex | 427 \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 D | basics.tex | 51 \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 D | QuantHeuristics.tex | 109 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 D | polytypicLib.sml | 10 (* 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 D | CODETREE_OPTIMISER.sml | 106 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 D | PmatchHeuristics.sml | 38 (* 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 D | file_readerLib.sml | 106 (* helper functions *) 216 val _ = f (" Total: " ^ names_count ^ " functions, " ^ inst_count ^ 233 " functions ("
|
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/ |
H A D | exor32.ml | 55 (* These functions are added to a couple of global lists. *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | ord-map-sig.sml | 8 * Extended by two functions "update" and "findSome" - Martin Erwig
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ord-map-sig.sml | 8 * Extended by two functions "update" and "findSome" - Martin Erwig
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | ord-map-sig.sml | 8 * Extended by two functions "update" and "findSome" - Martin Erwig
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Stream.sml | 12 (* Helper functions. *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/MISC/ |
H A D | eval-test.ml | 1 % File for testing the Lisp functions defined in hol/lisp/eval.l
|