Searched refs:function (Results 176 - 200 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/num/arith/src/
H A DSub_and_cond.sml26 fun failwith function =
28 origin_function = function,
198 (* enclose the subtraction operator. This function is not as delicate as it *)
211 (* Also eliminates the predecessor function, PRE. *)
H A DGen_arith.sml20 fun failwith function = raise (mk_HOL_ERR "Gen_arith" function "");
32 (* The internal function uses failure to denote that the expression *)
76 (* The function detects multiplications in which both of the arguments are *)
/seL4-l4v-master/HOL4/src/opentheory/postbool/
H A DLogging.sig35 [set_tyop_name_handler h] installs h as the function used to create an OpenTheory name from a HOL4 type operator name when the OpenTheoryMap does not already have a mapping for the HOL4 name.
/seL4-l4v-master/HOL4/src/parse/
H A DPretype.sig59 [mk_fun_ty (dom,rng)] Makes the pretype corresponding to the function space
/seL4-l4v-master/HOL4/src/pfl/examples/
H A Dzero.sml2 (* Constant zero function. *)
28 (* Indexed function definition *)
41 (* Domain of the function. *)
269 (* Theorem showing that exec BIG = zero in the domain of the function. *)
/seL4-l4v-master/HOL4/src/quotient/src/
H A Dquotient.sml19 (* This file defines the function "define_quotient_types", which takes *)
201 {abs} is a string, denoting the name of the new onto function from the
203 {rep} is a string, denoting the name of the new 1-1 function from the
278 Let each such set be represented by its characteristic function,
283 If P c, then c is a suitable function to represent an nty.
381 are one-to-one and onto. The ABS function is one-to-one on its
413 (* define function to yield representative objects of the new objects *)
426 (* define function to yield new objects from the base objects *)
710 message = "The following does not have the form of a simplification theorem for either\nrelation extension simplification or map function extension simplification:\n" ^
756 Let each such set be represented by its characteristic function,
[all...]
/seL4-l4v-master/HOL4/src/ring/src/
H A DringLib.sig31 * - Reify is a function to transform a list of ring terms into
/seL4-l4v-master/HOL4/src/simp/src/
H A DCond_rewr.sig21 ascending order, according to a term_lt function which places
/seL4-l4v-master/HOL4/tools/Holmake/
H A DSysteml.sig42 when fed to the compiler. For MoscowML, this is the identity function
/seL4-l4v-master/HOL4/tools/Holmake/mosml/
H A DHM_Cline.sml38 (* this fupdcore function is used internally to build command-line options *)
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dlink.sml47 (* returns function which takes a file name, invokes the parser on the file,
/seL4-l4v-master/HOL4/examples/CCS/
H A DCCSSyntax.sml115 (* Given a list of terms, the function build_sum builds a CCS term which is
130 the function sum_to_fun sumL ARBtm n returns a function which associates
200 (* Conversion for evaluating a relabelling function fc (in conditional form). *)
H A DObsCongrConv.sml26 (* Define the function OC_SUB_CONV. *)
63 (* Define the function OC_DEPTH_CONV. *)
67 (* Define the function OC_TOP_DEPTH_CONV. *)
74 (* Define the function OC_SUBST for substitution in OBS_CONGR terms. *)
H A DWeakLawsConv.sml99 (* Define the function OE_SUB_CONV. *)
150 (* Define the function OE_DEPTH_CONV. *)
154 (* Define the function OE_TOP_DEPTH_CONV. *)
161 (* Define the function OE_SUBST for substitution in WEAK_EQUIV terms. *)
/seL4-l4v-master/HOL4/examples/PSL/1.01/parser.mosmlyacc/
H A DLexer.lex25 (* Scan keywords as identifiers and use this function to distinguish them. *)
/seL4-l4v-master/HOL4/polyml/mlsource/
H A DBuildExport.sml27 (* This function is the root of the "pre-built" compilers. It compiles in
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DLiteralNet.sml58 (* These function return OVER-APPROXIMATIONS! *)
H A DPortableMlton.sml49 (* Timing function applications. *)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_synthesisLib.sml34 (* the main synthesis function: shallow -> deep *)
/seL4-l4v-master/HOL4/examples/muddy/
H A Dfdd.sig38 relates to C types and function declarations in fdd.h:
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DLiteralNet.sml58 (* These function return OVER-APPROXIMATIONS! *)
H A DPortableMlton.sml49 (* Timing function applications. *)
/seL4-l4v-master/HOL4/src/AI/proof_search/
H A DpsMCTS.sig29 (* search function *)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCodeSig.sml41 | BICEval of (* Evaluate a function with an argument list. *)
43 function: backendIC,
68 | BICBeginLoop of (* Start of tail-recursive inline function. *)
71 | BICLoop of (backendIC * argumentType) list (* Jump back to start of tail-recursive function. *)
/seL4-l4v-master/HOL4/src/Boolify/src/
H A DEncode.sml68 (* Term encoding, as a function of types. The function gamma maps type *)
70 (* means failure. The function theta maps a type variable (say 'a) to a term *)
257 | NONE => (HOL_MESG("Couldn't define encode function for type "

Completed in 148 milliseconds

1234567891011>>