Searched refs:defines (Results 1 - 25 of 104) sorted by relevance
12345
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | msvcc.sh | 115 defines="$defines $1" 138 defines="$defines -D${name}='$value'" 143 defines="$defines $1" 235 echo "$cl -nologo -EP $includes $defines $src > $ppsrc" 236 "$cl" -nologo -EP $includes $defines $src > $ppsrc || exit $?
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | gr.sml | 10 GraphNode defines type of graph nodes 11 GraphExceptions defines graph exceptions
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr.sml | 10 GraphNode defines type of graph nodes 11 GraphExceptions defines graph exceptions
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr.sml | 10 GraphNode defines type of graph nodes 11 GraphExceptions defines graph exceptions
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sig | 8 (* mc_define defines a function and puts the definition on a queue
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_coretypesScript.sml | 10 This theory defines the types and operations over these types for the PowerPC model.
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_coretypesScript.sml | 10 This theory defines the types and operations over these types for the x86 model.
|
H A D | x86_astScript.sml | 11 This theory defines the abstract syntax tree (AST) for x86 instructions. It uses
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_coretypesScript.sml | 10 This theory defines the types and operations over these types for the x64 model.
|
H A D | x64_astScript.sml | 11 This theory defines the abstract syntax tree (AST) for x64 instructions. It uses
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/imp/ |
H A D | impScript.sml | 11 This file defines a funcional big-step semantics for the IMP languages 46 (* The following function defines the semantics of statement evaluation.
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | imported_acl2Script.sml | 2 (* This file defines a type of s-expressions and various constants and *)
|
H A D | acl2_packageScript.sml | 5 (* Also defines a predicate VALID_PKG_TRIPLES from Matt Kaufmann that *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | values.ml | 7 % This theory defines word widths, dimensions of memories, some %
|
H A D | next.ml | 7 % This theory defines the 'NEXT' relation which relates a time %
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics_ZF/document/ |
H A D | ZF.tex | 322 always meaningful, but we do not know its value unless $P[x]$ defines it 332 Isabelle's set theory defines two {\bf bounded quantifiers}: 427 The Isabelle theory defines \cdx{Replace} to apply 432 \isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the 1036 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual 1074 Theory \thydx{Sum} defines the disjoint union of two sets, with 1098 Theory \thydx{QPair} defines a notion of ordered pair that admits 1100 {\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the 1162 set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest 1179 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines th [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics_ZF/document/ |
H A D | ZF.tex | 322 always meaningful, but we do not know its value unless $P[x]$ defines it 332 Isabelle's set theory defines two {\bf bounded quantifiers}: 427 The Isabelle theory defines \cdx{Replace} to apply 432 \isa{Replace} is much easier to use than \isa{PrimReplace}; it defines the 1036 Theory \thydx{Bool} defines $\{0,1\}$ as a set of booleans, with the usual 1074 Theory \thydx{Sum} defines the disjoint union of two sets, with 1098 Theory \thydx{QPair} defines a notion of ordered pair that admits 1100 {\tt<$a$;$b$>}. It also defines the eliminator \cdx{qsplit}, the 1162 set (Fig.\ts\ref{zf-fixedpt}). The theory defines least and greatest 1179 Theory \texttt{Finite} (Figure~\ref{zf-fin}) defines th [all...] |
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | for_ndScript.sml | 7 This file defines a FOR language that's very similar to the language
|
/seL4-l4v-10.1.1/HOL4/examples/MLsyntax/ |
H A D | MLScript.sml | 2 * This example defines the abstract syntax for a simple ML-like language, *
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/ |
H A D | adder-in-Model.ml | 11 % This file defines a HOL specification of an adder that mimics the %
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 2 * This example defines the abstract syntax for a simple ML-like language,
|
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | numScript.sml | 34 (* `IS_NUM:ind->bool` defines the subset of `:ind` used to represent *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 34 for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 34 for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the
|
/seL4-l4v-10.1.1/l4v/camkes/glue-spec/document/ |
H A D | intro.tex | 67 \autoref{h:connector} defines the intermediate event and memory components
|
Completed in 129 milliseconds
12345