Searched refs:extension (Results 1 - 25 of 67) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/polyml/
H A Dpolyc.in58 echo " -c Compile but do not link. The object file is written to the source file with .$SUFFIX extension."
73 extension="${1##*.}"
74 case "$extension" in
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DUTuple.sml38 (* extension *)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DUTuple.sml38 (* extension *)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/
H A DUTuple.sml38 (* extension *)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dexporter.cpp434 #define MAX_EXTENSION 4 // The longest extension we may need to add is ".obj"
486 static void exporter(TaskData *taskData, Handle fileName, Handle root, const TCHAR *extension, Exporter *exports) argument
488 size_t extLen = _tcslen(extension);
494 // Does it already have the extension? If not add it on.
495 if (length < extLen || _tcscmp(fileNameBuff + length - extLen, extension) != 0)
496 _tcscat(fileNameBuff, extension);
618 const TCHAR *extension = _T(".obj"); // Windows local
620 const char *extension = ".o"; // Cygwin
624 taskData->saveVec.push(args->WordP()->Get(1)), extension, &exports);
627 const char *extension
664 const TCHAR *extension = _T(".obj"); // Windows local
[all...]
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DQbfCertificate.sml31 datatype extension = ITE of literal * literal * literal type
37 VALID of (vindex, extension) Redblackmap.dict
68 "unexpected input after '0'-terminated list of extension literals"
71 "missing '0' terminator after extension literals"
74 (* (vindex, extension) dict -> string list -> (vindex, extension) dict *)
75 fun extension ext [vindex, "I", lit1, lit2, lit3] = function
78 | extension ext (vindex :: "A" :: lits) =
81 | extension _ _ =
82 raise ERR "read_certificate_file" "extension
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex46 functions by domain extension. The second part contains some lemmas about the
47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
/seL4-l4v-10.1.1/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex46 functions by domain extension. The second part contains some lemmas about the
47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
/seL4-l4v-10.1.1/HOL4/Manual/Logic/
H A Dsemantics.tex679 \index{extension, of HOL logic@extension, of \HOL{} logic!abstract form of}
683 extension\/}\index{extension, of theory} of a theory ${\cal T}$ if:
717 Section~\ref{tyspecs}).\footnote{This theory extension mechanism is
757 \index{extension, of HOL logic@extension, of \HOL{} logic!by constant definition|(}
777 Sig}_{\cal T}$, then the {\em definitional extension\/}\index{constant definition extension, of HOL logic@constant definition extension, o
[all...]
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHolmake_tools.sig78 val extendp : {base : t, extension : string} -> t
79 val extend : {base : t, extension : t} -> t
H A DHolmake_tools.sml470 fun extendp {base = {relpath, absdir}, extension} = let
474 if Path.isAbsolute extension then
475 {relpath = NONE, absdir = Path.mkCanonical extension}
478 NONE => {absdir = absdir + extension, relpath = NONE}
479 | SOME p => {relpath = SOME (p + extension),
480 absdir = absdir + extension}
483 fun extend {base, extension} =
484 extendp {base = base, extension = toString extension}
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DBUILTINS.sml58 | SignedToLongWord (* Convert a tagged value to a LargeWord with sign extension. *)
59 | UnsignedToLongWord (* Convert a tagged value to a LargeWord without sign extension. *)
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DnormalFormsScript.sml7 (* If two functions f and g agree on their extension point EXT_POINT f g, *)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dproblems.sml978 (!x y z v. between x y (extension x y z v)) /\
979 (!x y z v. equidistant x (extension y x z v) z v) /\
990 (!x y z v. between x y (extension x y z v)) /\
991 (!x y z v. equidistant x (extension y x z v) z v) /\
1064 (!x y z v w. ~(x = y) \/ extension x z v w = extension y z v w) /\
1065 (!x y z v w. ~(x = y) \/ extension z x v w = extension z y v w) /\
1066 (!x y z v w. ~(x = y) \/ extension z v x w = extension
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dproblems.sml978 (!x y z v. between x y (extension x y z v)) /\
979 (!x y z v. equidistant x (extension y x z v) z v) /\
990 (!x y z v. between x y (extension x y z v)) /\
991 (!x y z v. equidistant x (extension y x z v) z v) /\
1064 (!x y z v w. ~(x = y) \/ extension x z v w = extension y z v w) /\
1065 (!x y z v w. ~(x = y) \/ extension z x v w = extension z y v w) /\
1066 (!x y z v w. ~(x = y) \/ extension z v x w = extension
[all...]
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/
H A Dsemantics.tex679 \index{extension, della logica HOL@extension, della logica \HOL{}!forma astratta di}
683 estensione\/}\index{extension, of theory} di una teoria ${\cal T}$ se:
756 \index{extension, della logica HOL@extension, della logica \HOL{}!by constant definition|(}
776 Sig}_{\cal T}$, allora l'{\em estensione definizionale\/}\index{constant definition extension, della logica HOL@constant definition extension, della logica \HOL{}!forma astratta di} di ${\cal T}$
860 \index{extension, della logica HOL@extension, della logica \HOL{}!by constant definition|)}
863 \index{extension, dell
[all...]
/seL4-l4v-10.1.1/isabelle/src/Doc/Functions/document/
H A Dintro.tex36 extension: Recursive definitions are internally transformed into a
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A Dpreface.tex30 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Functions/document/
H A Dintro.tex36 extension: Recursive definitions are internally transformed into a
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/
H A Dpreface.tex30 \item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
/seL4-l4v-10.1.1/HOL4/src/meson/test/
H A Dselftest.sml789 (!X Y W V. between(X,Y,extension(X,Y,W,V))) /\
790 (!X Y W V. equidistant(Y,extension(X,Y,W,V),W,V)) /\
819 (!X Y V1 V2 V3. equal(X,Y) ==> equal(extension(X,V1,V2,V3),extension(Y,V1,V2,V3))) /\
820 (!X V1 Y V2 V3. equal(X,Y) ==> equal(extension(V1,X,V2,V3),extension(V1,Y,V2,V3))) /\
821 (!X V1 V2 Y V3. equal(X,Y) ==> equal(extension(V1,V2,X,V3),extension(V1,V2,Y,V3))) /\
822 (!X V1 V2 V3 Y. equal(X,Y) ==> equal(extension(V1,V2,V3,X),extension(V
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_astScript.sml55 | Pextsb of ireg => ireg (* 8-bit sign extension *)
56 | Pextsh of ireg => ireg (* 16-bit sign extension *)
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DCursor.sml111 (* ML extension - simpler than having a separate function. *)
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/
H A Dquotient.tex399 their extension for aggregate and function types,
401 and quotient extension theorems
404 %The quotient extension theorem for function types
582 there is a natural extension of {\it E\/} to values of lists of $\tau$.
703 for the base types and equivalence extension theorems for type operators
706 {\it Equivalence extension theorems\/} for type operators
734 Using the above relation extension operators,
743 have the following equivalence extension theorems:
1503 quotient operation, but also lift by extension a number of other
1531 To accomplish this, the tool uses {\it quotient extension theorem
[all...]
/seL4-l4v-10.1.1/HOL4/src/rational/
H A DintExtensionScript.sml5 * extension of the theory of integers

Completed in 288 milliseconds

123