| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibSimple.sml | 17 (concat [Globals.HOLDIR, "/src/quantHeuristics"])::
|
| H A D | quantHeuristicsTools.sml | 17 (concat [Globals.HOLDIR, "/src/quantHeuristics"])::
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/poly/ |
| H A D | holfoot_command_line.sml | 2 use (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/poly/header.sml");
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceSyntax.sml | 6 loadPath := (Globals.HOLDIR ^ "/examples/separationLogic/src") ::
|
| H A D | separationLogicLib.sml | 7 (Globals.HOLDIR ^ "/examples/separationLogic/src") ::
8 (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot") ::
932 val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot/EXAMPLES/"]
|
| H A D | latticeScript.sml | 6 (Globals.HOLDIR ^ "/examples/separationLogic/src") ::
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | testTypesScript.sml | 132 (* Some examples from src/datatype/jrh.test *)
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
| H A D | psl_to_rltlScript.sml | 8 loadPath := (concat home_dir "src/deep_embeddings") ::
9 (concat home_dir "src/translations") ::
10 (concat home_dir "src/tools") ::
|
| H A D | translationsLib.sml | 9 loadPath := (concat home_dir "src/deep_embeddings") ::
10 (concat home_dir "src/translations") ::
11 (concat home_dir "src/tools") ::
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | QuantHeuristics.tex | 91 \holtxt{src/quantHeuristics}. The entry point to the framework is the
246 The unwind library\footnote{see \texttt{src/simp/src/Unwind.sml}} on the other hand is limited, but fast.
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
| H A D | armScript.sml | 386 and src = if I then SND (IMMEDIATE F opnd) else REG_READ reg mode Rm in value
388 (\i b. (28 <= i) /\ (if bit19 then src %% i else b) \/
390 (i <= 7) /\ (if bit16 /\ ~USER mode then src %% i else b))
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | armScript.sml | 432 and src = if I then SND (IMMEDIATE F opnd) else REG_READ r.reg mode Rm in value
434 (\i b. (28 <= i) /\ (if bit19 then src ' i else b) \/
436 (i <= 7) /\ (if bit16 /\ ~USER mode then src ' i else b))
|
| H A D | arm_rulesScript.sml | 646 Abbrev (src = if IS_MSR_IMMEDIATE op2 then
652 28 <= i /\ (if flags then src ' i else b) \/
655 (if ctrl /\ ~USER mode then src ' i else b)))``]
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 7 use (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/header.sml");
10 (concat [Globals.HOLDIR, "/src/quantHeuristics"]) ::
11 (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) ::
12 (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) ::
53 val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot/EXAMPLES/automatic/"]
2961 val examplesDir = concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot/EXAMPLES"]
|
| H A D | holfoot_pp_print.sml | 7 (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) ::
8 (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) ::
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
| H A D | ibmScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") ::
8 (concat home_dir "src/translations") ::
9 (concat home_dir "src/tools") ::
|
| /seL4-l4v-10.1.1/HOL4/src/TeX/ |
| H A D | holindex.sml | 518 val basename = Globals.HOLDIR ^ "/src/TeX/holindex-demo";
|
| /seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
| H A D | hhTranslate.sml | 28 val hh_dir = HOLDIR ^ "/src/holyhammer"
|
| H A D | holyHammer.sml | 54 val hh_dir = pathl [HOLDIR,"src","holyhammer"];
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake_types.sml | 362 ("MLYACC", [VREF "protect $(HOLDIR)/tools/mlyacc/src/mlyacc.exe"]),
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/ |
| H A D | testEncode.sml | 55 (* Some examples from src/datatype/jrh.test *)
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
| H A D | alternating_omega_automataScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") ::
8 (concat home_dir "src/tools") :: !loadPath;
|
| H A D | ctl_starScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") ::
8 (concat home_dir "src/tools") :: !loadPath;
|
| H A D | full_ltlScript.sml | 7 loadPath := (concat home_dir "src/deep_embeddings") ::
8 (concat home_dir "src/tools") :: !loadPath;
|
| H A D | prop_logicScript.sml | 7 loadPath := (home_dir ^ "src/deep_embeddings") ::
8 (home_dir ^ "src/tools") :: !loadPath;
|