Searched refs:defines (Results 1 - 25 of 104) sorted by relevance

12345

/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dmsvcc.sh115 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 Dgr.sml10 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 Dgr.sml10 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 Dgr.sml10 GraphNode defines type of graph nodes
11 GraphExceptions defines graph exceptions
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sig8 (* 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 Dppc_coretypesScript.sml10 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 Dx86_coretypesScript.sml10 This theory defines the types and operations over these types for the x86 model.
H A Dx86_astScript.sml11 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 Dx64_coretypesScript.sml10 This theory defines the types and operations over these types for the x64 model.
H A Dx64_astScript.sml11 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 DimpScript.sml11 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 Dimported_acl2Script.sml2 (* This file defines a type of s-expressions and various constants and *)
H A Dacl2_packageScript.sml5 (* Also defines a predicate VALID_PKG_TRIPLES from Matt Kaufmann that *)
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/
H A Dvalues.ml7 % This theory defines word widths, dimensions of memories, some %
H A Dnext.ml7 % This theory defines the 'NEXT' relation which relates a time %
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex322 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 DZF.tex322 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 Dfor_ndScript.sml7 This file defines a FOR language that's very similar to the language
/seL4-l4v-10.1.1/HOL4/examples/MLsyntax/
H A DMLScript.sml2 * This example defines the abstract syntax for a simple ML-like language, *
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/
H A Dadder-in-Model.ml11 % This file defines a HOL specification of an adder that mimics the %
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/
H A Dexample.sml2 * This example defines the abstract syntax for a simple ML-like language,
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DnumScript.sml34 (* `IS_NUM:ind->bool` defines the subset of `:ind` used to represent *)
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A Dsyntax.tex34 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 Dsyntax.tex34 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 Dintro.tex67 \autoref{h:connector} defines the intermediate event and memory components

Completed in 100 milliseconds

12345