/seL4-l4v-master/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-master/HOL4/examples/dev/sw/ |
H A D | UTuple.sml | 38 (* extension *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | UTuple.sml | 38 (* extension *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | UTuple.sml | 38 (* extension *)
|
/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | GraphExtra.sml | 22 val fp = hmdir.extendp {base = master_dir, extension = s}
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | exporter.cpp | 514 #define MAX_EXTENSION 4 // The longest extension we may need to add is ".obj" 584 static void exporter(TaskData *taskData, Handle fileName, Handle root, const TCHAR *extension, Exporter *exports) argument 586 size_t extLen = _tcslen(extension); 592 // Does it already have the extension? If not add it on. 593 if (length < extLen || _tcscmp(fileNameBuff + length - extLen, extension) != 0) 594 _tcscat(fileNameBuff, extension); 721 const TCHAR *extension = _T(".obj"); // Windows local 723 const char *extension = ".o"; // Cygwin 727 taskData->saveVec.push(args->WordP()->Get(1)), extension, &exports); 730 const char *extension 767 const TCHAR *extension = _T(".obj"); // Windows local [all...] |
/seL4-l4v-master/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-master/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-master/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-master/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-master/seL4/include/arch/riscv/arch/machine/ |
H A D | registerset.h | 101 #error Unknown RISCV FPU extension
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_tools.sig | 112 val extendp : {base : t, extension : string} -> t 113 val extend : {base : t, extension : t} -> t
|
H A D | Holmake_tools.sml | 519 fun extendp {base = {relpath, absdir}, extension} = let 523 if Path.isAbsolute extension then 524 {relpath = NONE, absdir = Path.mkCanonical extension} 527 NONE => {absdir = absdir + extension, relpath = NONE} 528 | SOME p => {relpath = SOME (p + extension), 529 absdir = absdir + extension} 532 fun extend {base, extension} = 533 extendp {base = base, extension = toString extension} 645 val dir' = hmdir.extendp {base = hmdir.curdir(), extension [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | BUILTINS.sml | 59 | SignedToLongWord (* Convert a tagged value to a LargeWord with sign extension. *) 60 | UnsignedToLongWord (* Convert a tagged value to a LargeWord without sign extension. *)
|
/seL4-l4v-master/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-master/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-master/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-master/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-master/isabelle/src/Doc/Functions/document/ |
H A D | intro.tex | 36 extension: Recursive definitions are internally transformed into a
|
/seL4-l4v-master/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-master/l4v/isabelle/src/Doc/Functions/document/ |
H A D | intro.tex | 36 extension: Recursive definitions are internally transformed into a
|
/seL4-l4v-master/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-master/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-master/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-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Cursor.sml | 111 (* ML extension - simpler than having a separate function. *)
|