/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | modelCheckLib.sml | 8 loadPath := (concat home_dir "src/deep_embeddings") :: 9 (concat home_dir "src/translations") :: 10 (concat home_dir "src/tools") ::
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | translationsLibScript.sml | 8 loadPath := (concat home_dir "src/deep_embeddings") :: 9 (concat home_dir "src/translations") :: 10 (concat home_dir "src/tools") ::
|
H A D | alternating_omega_automata_to_automaton_formulaScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath;
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/mlton/ |
H A D | evalML.sml | 5 "src/portableML", "src/theoryML"]; 483 (* Taken from Joe Hurd's $HOLDIR/tools/mlton/src/mlibPortable.sml *)
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
H A D | BuildCommand.sml | 411 (Mosml_compile (objs, src), I) => 413 (toFile src)
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bvec.h | 137 bvec operator=(const bvec &src);
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | infinite_pathScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath;
|
H A D | kripke_structureScript.sml | 7 loadPath := (home_dir ^ "src/deep_embeddings") :: 8 (home_dir ^ "src/tools") :: !loadPath;
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Tptp.sml | 471 fun add ((src,arity),dest,m) = 473 val src = Name.fromString (toTptp (src,arity)) value 475 NameArityMap.insert m ((src,arity),dest) 1930 val src = CnfClauseSource (name,clause) value 1932 val norm = addClauses role [(cl,src)] norm 2199 SOME src => src
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | Htmlsigs.sml | 82 fun scanident getc src = 86 val sus1 = skipWS getc src
|
H A D | Doc2Html.sml | 110 out "<A HREF = \"../../src-sml/htmlsigs/";
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Tptp.sml | 471 fun add ((src,arity),dest,m) = 473 val src = Name.fromString (toTptp (src,arity)) value 475 NameArityMap.insert m ((src,arity),dest) 1930 val src = CnfClauseSource (name,clause) value 1932 val norm = addClauses role [(cl,src)] norm 2199 SOME src => src
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | GdiBase.sml | 40 val NOTSRCERASE = W (0x001100A6 (* dest = (NOT src) AND (NOT dest) *))
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibAbbrev.sml | 16 (concat [Globals.HOLDIR, "/src/quantHeuristics"])::
|
H A D | quantHeuristicsLibParameters.sml | 17 (concat [Globals.HOLDIR, "/src/quantHeuristics"])::
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient_sumScript.sml | 50 src/sum/sumScript.sml. *)
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tacticToe.sml | 78 hide_out QUse.use (tactictoe_dir ^ "/src/infix_file.sml");
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sml | 945 val MOVUP_D_S_1 = sse ``dfn'MOVUP_D_S (double, xmm, xmm_reg (src))`` |> List.tl 948 val MOVSD_1 = sse ``dfn'MOVSD (xmm, xmm_reg (src))`` |> List.tl |> wv_to_v 950 val MOVSS_1 = sse ``dfn'MOVSS (xmm, xmm_reg (src))`` |> List.tl |> wv_to_v 958 val MOVQ_1 = sse ``dfn'MOVQ (xmm, xmm_reg (src))`` |> List.tl
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/examples/ |
H A D | verification.sml | 8 loadPath := ["../src"] @ !loadPath;
|
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | prehol.sml | 38 set up in src/0/Overlay.sml *)
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/ |
H A D | teaScript.sml | 219 (* HOLDIR/src/emit/ML *)
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootParser.sml | 7 (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) :: 8 (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) :: 14 use (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/hfheader.sml") 1262 val examplesDir = Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/EXAMPLES/"; 1266 val examplesDir = Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/EXAMPLES/";
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | parse_term.sml | 391 (fn (lower_right,src) => 392 insert ((lower_right,true), lefttok) (PM_GREATER src)) 450 app (fn (lower_right,src) => 451 insert ((lower_right,true), TypeColon) (PM_GREATER src)) 459 app (fn (lower_right,src) => 460 insert ((lower_right,true), left_tok) (PM_GREATER src))
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceBaseFunctor.sml | 74 (Globals.HOLDIR ^ "/examples/separationLogic/src") :: 75 (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot") ::
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | interpret.cpp | 1910 PolyObject *src = (PolyObject*)((*sp).AsCodePtr() + srcOffset); local 1911 for (POLYUNSIGNED u = 0; u < length; u++) dest->Set(destIndex+u, src->Get(srcIndex+u)); 1922 POLYCODEPTR src = (*sp).AsCodePtr(); local 1923 memcpy(dest+destOffset, src+srcOffset, length);
|