/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | polyc.in | 58 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 D | UTuple.sml | 38 (* extension *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | UTuple.sml | 38 (* extension *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | UTuple.sml | 38 (* extension *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | exporter.cpp | 434 #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 D | QbfCertificate.sml | 31 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 D | root.tex | 46 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 D | root.tex | 46 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 D | semantics.tex | 679 \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 D | Holmake_tools.sig | 78 val extendp : {base : t, extension : string} -> t 79 val extend : {base : t, extension : t} -> t
|
H A D | Holmake_tools.sml | 470 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 D | BUILTINS.sml | 58 | 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 D | normalFormsScript.sml | 7 (* 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 D | problems.sml | 978 (!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 D | problems.sml | 978 (!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 D | semantics.tex | 679 \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 D | intro.tex | 36 extension: Recursive definitions are internally transformed into a
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | preface.tex | 30 \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 D | intro.tex | 36 extension: Recursive definitions are internally transformed into a
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | preface.tex | 30 \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 D | selftest.sml | 789 (!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 D | ppc_astScript.sml | 55 | 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 D | Cursor.sml | 111 (* ML extension - simpler than having a separate function. *)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 399 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 D | intExtensionScript.sml | 5 * extension of the theory of integers
|