Searched refs:functions (Results 76 - 100 of 695) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/
H A Dsyscalls_syscall.h17 #include <sel4/arch/functions.h>
H A Dsyscalls_sysenter.h17 #include <sel4/arch/functions.h>
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/
H A Ddescription.tex8 restricted quantifiers, and a set of ML functions for dealing with
14 overview of the ML functions available in the library and a
16 manual for all ML functions appears in Chapter~2. The last chapter
169 \section{ML functions}
171 The ML functions available when this library is loaded can be divided
172 into six groups: conditional rewriting tools, syntax functions,
180 which can be loaded into \HOL\ without loading other functions in this
249 implemented. The details of the tactics and search functions can be
268 \subsection{Syntax functions}
331 convenience, the following ML functions ar
[all...]
/seL4-l4v-10.1.1/graph-refine/
H A Dsyntax.py10 # and graph functions (functions in graph-language format).
65 A graph program consists of a number of functions, each
70 - 'Call' makes calls to functions.
74 - Function blocks introduce functions.
113 so functions will typically have global objects such as the heap as both input
116 The function block may end immediately, for functions with unspecified body,
910 # parsing code for types, expressions, structs and functions
1113 functions = {}
1146 assert fname not in functions, fnam
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/
H A DNotXor32.ml23 (* More boilerplate. Declaring combinational logic functions. *)
/seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sig8 This function translates all the functions defined in defs to
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/
H A DelsaUtils.sig55 val mapshape :{functions:('a list -> 'b) list,
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A Drich_listSyntax.sml8 Syntax functions for rich_list
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/
H A DLogging.sig37 [reset_tyop_name_handler()] and [reset_const_name_handler()] remove these custom functions (reverting to the default behaviour of raising an exception when a mapping does not exist).
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DHOLPP.sml9 (* the functions and data for actually doing printing. *)
H A DStreams.sml3 (* DESCRIPTION : Datatype and functions for streams (lazy lists). *)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DCache.sig18 functions where it is inappropriate to have hypotheses that don't
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/
H A Dnomdatatype.sig38 (* datatype utility functions *)
/seL4-l4v-10.1.1/HOL4/examples/muddy/
H A Dfdd.sig19 (* Structure fdd implements BuDDy's fdd functions.
/seL4-l4v-10.1.1/HOL4/Manual/Reference/
H A DMakefile66 @echo "\section{Theorems about functions}" >> theorems.tex
67 /bin/sh bin/doc-to-tex ${D2TSED} ${Helpd}/THEOREMS/functions theorems.tex
87 (cd $(THMDIR)functions; $(MAKEDOC) fun) ;
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/
H A DKripkeScript.sml30 functions on lists (commented out for compilation)
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dimported_acl2Script.sml3 (* functions on this type (t, nil, car, cdr, cons etc). *)
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Droot.tex19 \index{termination|see{functions, total}}
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Droot.tex19 \index{termination|see{functions, total}}
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DLiteral.sml41 fun functions lit = Atom.functions (atom lit); function
223 val functions = value
225 fun f (lit,set) = NameAritySet.union set (Literal.functions lit)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DLiteral.sml41 fun functions lit = Atom.functions (atom lit); function
223 val functions = value
225 fun f (lit,set) = NameAritySet.union set (Literal.functions lit)
/seL4-l4v-10.1.1/HOL4/src/coretypes/pair-Manual/
H A Ddescription.tex43 The table below sets out all the standard \HOL\ functions for which the
169 The pair library also contains many functions for which there are no
170 analogous nonpaired functions.
174 Before you can use any of the functions described in this manual,
192 The first design decision is that all the functions for dealing with paired
194 For the purposes of such functions, a pair may be an arbitrary
257 including optimisations and suggestions for new functions.
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DLibraryIOSupport.sml2 Title: Standard Basis Library: IO Support functions
197 (* Create the primitive IO functions and add the higher layers.
218 We have to handle that. The blocking functions can be
234 (* Unlike the other functions "avail" is a function returning
337 We have to handle that. The blocking functions can be
349 (* Unlike the other functions "avail" is a function returning
421 (* Many of the IO functions need a mutex so we include this here.
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A Dgr_t.sml83 (functions to be passed as arguments to M.update)
154 (* exported functions *)
245 (* exported functions *)
321 (* exported functions *)
362 (* exported functions *)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A Dgr_t.sml83 (functions to be passed as arguments to M.update)
154 (* exported functions *)
245 (* exported functions *)
321 (* exported functions *)
362 (* exported functions *)

Completed in 238 milliseconds

1234567891011>>