Searched refs:functions (Results 201 - 225 of 695) sorted by relevance
1234567891011>>
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Problem.sml | 106 fun f (cl,set) = NameAritySet.union set (LiteralSet.functions cl)
|
H A D | Tptp.sig | 25 (* Interpreting TPTP functions and relations in a finite model. *)
|
H A D | problems2tptp.sml | 21 (* Helper functions. *)
|
H A D | Tptp.sml | 16 [(* Mapping TPTP functions to infix symbols *) 41 (* Interpreting TPTP functions and relations in a finite model. *) 103 (* Helper functions. *) 444 (* Interpreting TPTP functions and relations in a finite model. *) 589 | functionsLiteral (Literal lit) = Literal.functions lit; 871 | FofFormulaBody fm => Formula.functions fm; 918 Normalize.Axiom fm => Formula.functions fm 919 | Normalize.Definition (_,fm) => Formula.functions fm 927 Proof.Axiom cl => LiteralSet.functions cl 928 | Proof.Assume atm => Atom.functions at [all...] |
/seL4-l4v-10.1.1/l4v/proof/infoflow/tools/ |
H A D | authority2infoflow-CaML.ml | 13 (* This file contains the functions building the tool that translates AUTHORITY GRAPHS into INFOFLOW POLICY GRAPHS *) 28 (* We define a bunch of elementary functions *) 311 (* first some basic functions *) 427 (* we define 2 functions mapping the labels in the infoflow graph to int, and back to string *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Formula.sig | 43 val functions : formula -> NameAritySet.set value
|
H A D | Literal.sig | 39 val functions : literal -> NameAritySet.set value
|
H A D | Problem.sml | 106 fun f (cl,set) = NameAritySet.union set (LiteralSet.functions cl)
|
H A D | Tptp.sig | 25 (* Interpreting TPTP functions and relations in a finite model. *)
|
H A D | problems2tptp.sml | 21 (* Helper functions. *)
|
H A D | Tptp.sml | 16 [(* Mapping TPTP functions to infix symbols *) 41 (* Interpreting TPTP functions and relations in a finite model. *) 103 (* Helper functions. *) 444 (* Interpreting TPTP functions and relations in a finite model. *) 589 | functionsLiteral (Literal lit) = Literal.functions lit; 871 | FofFormulaBody fm => Formula.functions fm; 918 Normalize.Axiom fm => Formula.functions fm 919 | Normalize.Definition (_,fm) => Formula.functions fm 927 Proof.Axiom cl => LiteralSet.functions cl 928 | Proof.Assume atm => Atom.functions at [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 218 (* Process a list of possibly mutually recursive functions and identify those that 330 (* Generate a range of addresses for any functions that have to 417 (* Generate functions for expressions that have been used more than 3 times. *) 520 (* Some functions are special e.g. overloaded and type-specific functions. 998 let (* Code-generate the eq and print functions for the abstype first 1134 (* Each function may result in either one or two functions 1138 generate two mutually recursive functions. A function 1151 (* Create a list of addresses for the functions. This is the address 1153 These may be changed for polymorphic functions bu [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | conv.tex | 55 collection of \ML\ functions enabling users to define new conversions 56 (as well as new rules and tactics) as functions of existing ones. 84 fact, some ML functions have names with the suffix `{\tt \_CONV}' 234 The functions \ml{THENC} and \ml{ORELSEC} are used to define the 409 a conversion can be converted to a rule or a tactic, using the functions 486 \index{conversions!functions for building|(} 491 of how functions are built using conversions. The section culminates 497 in building functions. 534 in building functions. 605 immediate subterms of a term. These use the \ML\ functions [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | funcCall.sml | 21 (* Pre-defined variables and functions *) 93 (* Find all modified registers and the next available memory slot for all functions *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
H A D | test.sml | 91 (* Inline expansion of anonymous functions *) 113 (* Inline expansion of named functions stored in env *)
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Library.sml | 3 (* Common auxiliary functions, tracing *) 166 (* creates a dictionary that maps strings to lists of parsing functions *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibCanon.sml | 24 (* Helper functions. *) 224 val funs = functions fm
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient_sumScript.sml | 32 (* the corresponding functions/relations of the constituent subtypes *) 49 (* for SUM of ABS / REP functions, use infix ++, defined in
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | GetOpt.sml | 38 (* helper functions *) 89 (* Some error handling functions *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_semanticsScript.sml | 44 (* Some utility values and functions *) 171 (* Label-defined functions share the same namespace). *)
|
/seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
H A D | preface.tex | 46 called \LCF\ (logic for computable functions), which was intended for 48 functions. The interface of the logic to the meta-language was made
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSSyntax.sml | 21 (* Auxiliary ML functions for dealing with CCS syntax *) 139 (* Auxiliary ML functions for dealing with CCS syntax *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | x86assembly_gas32.S | 48 # Macro to begin the hand-coded functions
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BaseCodeTreeSig.sml | 82 (* Built-in functions. *) 139 inline function. Tuple entries are functions from an integer
|
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 46 (* Property tag to indicate which arguments to a function are functions 91 functions passed in without requiring a full heap closure. *) 297 in working out the use-counts and whether the functions 298 (they should be functions) need closures. A function will 321 we don't copy the non-local lists of functions. *) 336 functions apart from those of the closures themselves. 338 iterate until all the functions which need full closures 783 (* If a heap closure is needed then any functions referred to
|
Completed in 238 milliseconds
1234567891011>>