/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/ |
H A D | syscalls_syscall.h | 17 #include <sel4/arch/functions.h>
|
H A D | syscalls_sysenter.h | 17 #include <sel4/arch/functions.h>
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | description.tex | 8 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 D | syntax.py | 10 # 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 D | NotXor32.ml | 23 (* More boilerplate. Declaring combinational logic functions. *)
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sig | 8 This function translates all the functions defined in defs to
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/ |
H A D | elsaUtils.sig | 55 val mapshape :{functions:('a list -> 'b) list,
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | rich_listSyntax.sml | 8 Syntax functions for rich_list
|
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
H A D | Logging.sig | 37 [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 D | HOLPP.sml | 9 (* the functions and data for actually doing printing. *)
|
H A D | Streams.sml | 3 (* DESCRIPTION : Datatype and functions for streams (lazy lists). *)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Cache.sig | 18 functions where it is inappropriate to have hypotheses that don't
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
H A D | nomdatatype.sig | 38 (* datatype utility functions *)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/ |
H A D | fdd.sig | 19 (* Structure fdd implements BuDDy's fdd functions.
|
/seL4-l4v-10.1.1/HOL4/Manual/Reference/ |
H A D | Makefile | 66 @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 D | KripkeScript.sml | 30 functions on lists (commented out for compilation)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | imported_acl2Script.sml | 3 (* functions on this type (t, nil, car, cdr, cons etc). *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | root.tex | 19 \index{termination|see{functions, total}}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | root.tex | 19 \index{termination|see{functions, total}}
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Literal.sml | 41 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 D | Literal.sml | 41 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 D | description.tex | 43 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 D | LibraryIOSupport.sml | 2 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 D | gr_t.sml | 83 (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 D | gr_t.sml | 83 (functions to be passed as arguments to M.update) 154 (* exported functions *) 245 (* exported functions *) 321 (* exported functions *) 362 (* exported functions *)
|