Searched refs:functions (Results 201 - 225 of 695) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DProblem.sml106 fun f (cl,set) = NameAritySet.union set (LiteralSet.functions cl)
H A DTptp.sig25 (* Interpreting TPTP functions and relations in a finite model. *)
H A Dproblems2tptp.sml21 (* Helper functions. *)
H A DTptp.sml16 [(* 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 Dauthority2infoflow-CaML.ml13 (* 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 DFormula.sig43 val functions : formula -> NameAritySet.set value
H A DLiteral.sig39 val functions : literal -> NameAritySet.set value
H A DProblem.sml106 fun f (cl,set) = NameAritySet.union set (LiteralSet.functions cl)
H A DTptp.sig25 (* Interpreting TPTP functions and relations in a finite model. *)
H A Dproblems2tptp.sml21 (* Helper functions. *)
H A DTptp.sml16 [(* 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 DCODEGEN_PARSETREE.sml218 (* 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 Dconv.tex55 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 DfuncCall.sml21 (* 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 Dtest.sml91 (* Inline expansion of anonymous functions *)
113 (* Inline expansion of named functions stored in env *)
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DLibrary.sml3 (* 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 DmlibCanon.sml24 (* Helper functions. *)
224 val funs = functions fm
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient_sumScript.sml32 (* 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 DGetOpt.sml38 (* helper functions *)
89 (* Some error handling functions *)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_semanticsScript.sml44 (* Some utility values and functions *)
171 (* Label-defined functions share the same namespace). *)
/seL4-l4v-10.1.1/HOL4/Manual/Logic/
H A Dpreface.tex46 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 DCCSSyntax.sml21 (* 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 Dx86assembly_gas32.S48 # Macro to begin the hand-coded functions
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBaseCodeTreeSig.sml82 (* Built-in functions. *)
139 inline function. Tuple entries are functions from an integer
H A DCODETREE_STATIC_LINK_AND_CASES.sml46 (* 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>>