/seL4-l4v-master/isabelle/Admin/Windows/Cygwin/isabelle/ |
H A D | rebaseall | 3 export PATH=/bin
|
H A D | postinstall | 3 export PATH=/bin
|
/seL4-l4v-master/l4v/isabelle/Admin/Windows/Cygwin/isabelle/ |
H A D | rebaseall | 3 export PATH=/bin
|
H A D | postinstall | 3 export PATH=/bin
|
/seL4-l4v-master/HOL4/src/opentheory/logging/ |
H A D | term2thm.cgi | 4 export PATH="$HOME/bin:$PATH"
|
/seL4-l4v-master/isabelle/Admin/Windows/Cygwin/ |
H A D | Cygwin-Terminal.bat | 5 set PATH=%CD%\bin;%PATH%
variable
|
/seL4-l4v-master/l4v/isabelle/Admin/Windows/Cygwin/ |
H A D | Cygwin-Terminal.bat | 5 set PATH=%CD%\bin;%PATH%
variable
|
/seL4-l4v-master/HOL4/examples/PSL/1.01/standalone/ |
H A D | pslcheck.sml | 5 * pslcheck [-all] -sere '<SERE>' -path '<PATH>' 6 * pslcheck [-all] -fl '<FL>' -path '<PATH>' 14 * pslcheck -sere '<SERE>' -path '<PATH>' 15 * pslcheck -fl '<FL>' -path '<PATH>' 21 * pslcheck -all -sere '<SERE>' -path '<PATH>' 28 * pslcheck -all -fl '<FL>' -path '<PATH>'
|
/seL4-l4v-master/isabelle/lib/Tools/ |
H A D | getenv | 80 export PATH_JVM="$(platform_path "$PATH")"
|
/seL4-l4v-master/l4v/isabelle/lib/Tools/ |
H A D | getenv | 80 export PATH_JVM="$(platform_path "$PATH")"
|
/seL4-l4v-master/graph-refine/scripts/ |
H A D | setup-HOL4.sh | 83 PATH=$HOL4_DIR/bin:$PATH build &>> $OUT
|
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | LTLScript.sml | 162 * PATH M s p is true iff p is a path of model M starting from s 166 `PATH M s p = (p 0 = s) /\ !i. M.R(p(i),p(i+1))`; 171 ``!M s p. s IN M.S /\ PATH M s p /\ MODEL M ==> !n. (p n) IN M.S``, 217 `SAT M f = !p. (p 0) IN M.S0 /\ PATH M (p 0) p ==> SEM M p f`; 348 ==> !p. PATH M s p ==> ?p'. PATH M' s' p' /\ !i. M'.S(p' i) /\ B(p i, p' i)``, 377 ==> !p'. PATH M' s' p' 378 ==> ?p. PATH M s p /\ !i. M.S(p i) /\ B(p i, p' i)``, 396 (!p. PATH M s p 397 ==> ?p'. PATH [all...] |
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ModelScript.sml | 88 (* PATH M s is true of path p iff p is a computation path of model M *) 92 `PATH M s w = 106 `COMPUTATION M w = ?s. s IN M.S0 /\ PATH M s w`;
|
H A D | UnclockedSemanticsScript.sml | 341 * PATH M s is true of p iff p is a computation path of M 357 ?p :: PATH M s. 361 ?p :: PATH M s. 368 ?p :: PATH M s.
|
H A D | ModelLemmasScript.sml | 80 ``(PATH M s (FINITE l) = 86 (PATH M s (INFINITE f) = 423 ``w IN PATH M s = PATH M s w``, 429 ``w IN COMPUTATION M = ?s. s IN M.S0 /\ PATH M s w``, 968 (PATH M s (FINITE l) = 1092 (* (PATH M (HD l) (FINITE l) = *) 1109 (PATH M (f 0) (INFINITE f) = 1134 (PATH M (ELEM w 0) w = 1248 ``PATH [all...] |
/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | UnclockedSemanticsScript.sml | 218 * PATH M p is true iff p is a path with respect to transition relation M.R 220 val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`; 234 ?p. PATH M p s /\ O_SEM M f (ELEM p 1)) 237 ?p. PATH M p s /\ 241 ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`;
|
/seL4-l4v-master/HOL4/examples/acl2/examples/LTL/ |
H A D | LTLScript.sml | 339 * PATH M s p is true iff p is a path of model M starting from s 343 `PATH M s p = (p 0 = s) /\ !i. M.R(p(i),p(i+1))`; 348 ``!M s p. s IN M.S /\ PATH M s p /\ MODEL M ==> !n. (p n) IN M.S``, 394 `SAT M f = !p. (p 0) IN M.S0 /\ PATH M (p 0) p ==> SEM M p f`; 525 ==> !p. PATH M s p ==> ?p'. PATH M' s' p' /\ !i. M'.S(p' i) /\ B(p i, p' i)``, 554 ==> !p'. PATH M' s' p' 555 ==> ?p. PATH M s p /\ !i. M.S(p i) /\ B(p i, p' i)``, 573 (!p. PATH M s p 574 ==> ?p'. PATH [all...] |
/seL4-l4v-master/graph-refine/seL4-example/ |
H A D | Makefile | 44 DECOMP_SCRIPT := $(shell PATH="${DECOMP_DIR}:${PATH}" sh -c "which decompile.py") 97 H4PATH := $(realpath ${HOL4_ROOT}/bin):${PATH} 118 cd ${TARGET_DIR} && PATH=${H4PATH} ${DECOMP_SCRIPT} --fast ./kernel --ignore=${IGNORES_${L4V_CONFIG}}
|
/seL4-l4v-master/HOL4/examples/PSL/1.01/parser/ |
H A D | ParserTools.sml | 413 * pslcheck [-all] -sere '<SERE>' -path '<PATH>' 414 * pslcheck [-all] -fl '<FL>' -path '<PATH>' 422 * pslcheck -sere '<SERE>' -path '<PATH>' 423 * pslcheck -fl '<FL>' -path '<PATH>' 429 * pslcheck -all -sere '<SERE>' -path '<PATH>' 436 * pslcheck -all -fl '<FL>' -path '<PATH>'
|
/seL4-l4v-master/HOL4/developers/ |
H A D | git-regression-build.sh | 149 echo "PATH: $PATH" &&
|
/seL4-l4v-master/HOL4/tools-poly/ |
H A D | smart-configure.sml | 148 case OS.Process.getEnv "PATH" of 174 else (* examine PATH variable *) 175 case OS.Process.getEnv "PATH" of 187 \to be in your PATH.\n\
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | ctlScript.sml | 320 * PATH M p is true iff p is a path with respect to transition relation M.R 322 val PATH_def = Define `PATH M p s = IS_INFINITE p /\ (ELEM p 0 = s) /\ (!n. M.R(ELEM p n, ELEM p (n+1)))`; 324 val PATH_INF = save_thm("PATH_INF",prove(``!M p s. PATH M p s ==> (PLENGTH p = INFINITY)``, 328 val ALL_IN_INF_PATH = save_thm("ALL_IN_INF_PATH",prove(``!M p s j. PATH M p s ==> j IN 0 to PLENGTH p``, 347 (CEX M X s = ?p. PATH M p s /\ (ELEM p 1) IN X) /\ 348 (CEU M (X1,X2) s = ?p. PATH M p s /\ ?k :: (0 to PLENGTH p). (ELEM p k) IN X2 /\ !j. j < k ==> (ELEM p j) IN X1) /\ 349 (CEG M X s = ?p. PATH M p s /\ !j :: (0 to PLENGTH p). (ELEM p j) IN X)
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | cheney_gcScript.sml | 73 (PATH (x,[]) s = T) /\ 74 (PATH (x,y::ys) s = PATH (y,ys) s /\ ?z d. (x,y,z,d) IN s \/ (x,z,y,d) IN s)`; 77 reachable r s i = (r = i) \/ ?p. PATH (r,p++[i]) s`; 605 ``!p r b i j m. PATH (r,p) (basic_abs(CUT (b,i) m)) /\ i <= j ==> 606 PATH (r,p) (basic_abs(CUT (b,j) m))``, 622 ``!ys x y z m. PATH(x,ys++[y])m /\ PATH(y,[z])m ==> PATH(x,ys++[y]++[z])m``, 745 \\ `PATH ( [all...] |
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | update.scala | 31 case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | update.scala | 31 case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
|