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

1234

/seL4-l4v-master/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-master/HOL4/examples/dev/sw/
H A DUTuple.sml38 (* extension *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DUTuple.sml38 (* extension *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DUTuple.sml38 (* extension *)
/seL4-l4v-master/HOL4/tools/Holmake/poly/
H A DGraphExtra.sml22 val fp = hmdir.extendp {base = master_dir, extension = s}
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dexporter.cpp514 #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 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-master/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-master/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-master/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-master/seL4/include/arch/riscv/arch/machine/
H A Dregisterset.h101 #error Unknown RISCV FPU extension
/seL4-l4v-master/HOL4/tools/Holmake/
H A DHolmake_tools.sig112 val extendp : {base : t, extension : string} -> t
113 val extend : {base : t, extension : t} -> t
H A DHolmake_tools.sml519 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 DBUILTINS.sml59 | 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 DnormalFormsScript.sml7 (* 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 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-master/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-master/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-master/isabelle/src/Doc/Functions/document/
H A Dintro.tex36 extension: Recursive definitions are internally transformed into a
/seL4-l4v-master/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-master/l4v/isabelle/src/Doc/Functions/document/
H A Dintro.tex36 extension: Recursive definitions are internally transformed into a
/seL4-l4v-master/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-master/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-master/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-master/HOL4/polyml/mlsource/extra/Win/
H A DCursor.sml111 (* ML extension - simpler than having a separate function. *)

Completed in 230 milliseconds

1234