/seL4-l4v-10.1.1/isabelle/Admin/Windows/Cygwin/isabelle/ |
H A D | rebaseall | 3 export PATH=/bin
|
H A D | postinstall | 3 export PATH=/bin
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Windows/Cygwin/isabelle/ |
H A D | rebaseall | 3 export PATH=/bin
|
H A D | postinstall | 3 export PATH=/bin
|
/seL4-l4v-10.1.1/HOL4/src/opentheory/logging/ |
H A D | term2thm.cgi | 4 export PATH="$HOME/bin:$PATH"
|
/seL4-l4v-10.1.1/isabelle/Admin/Windows/Cygwin/ |
H A D | Cygwin-Terminal.bat | 5 set PATH=%CD%\bin;%PATH%
variable
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Windows/Cygwin/ |
H A D | Cygwin-Terminal.bat | 5 set PATH=%CD%\bin;%PATH%
variable
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/lib/ |
H A D | target-libpath.exp | 105 if [info exists env(PATH)] { 106 set orig_path "$env(PATH)" 180 setenv PATH "$ld_library_path:$orig_path" 182 setenv PATH "$ld_library_path" 259 setenv PATH "$orig_path" 260 } elseif [info exists env(PATH)] { 261 unsetenv PATH
|
/seL4-l4v-10.1.1/isabelle/lib/Tools/ |
H A D | getenv | 80 export PATH_JVM="$(platform_path "$PATH")"
|
/seL4-l4v-10.1.1/l4v/isabelle/lib/Tools/ |
H A D | getenv | 80 export PATH_JVM="$(platform_path "$PATH")"
|
/seL4-l4v-10.1.1/graph-refine/scripts/ |
H A D | setup-HOL4.sh | 85 PATH=$HOL4_DIR/bin:$PATH build &>> $OUT
|
/seL4-l4v-10.1.1/l4v/spec/cspec/c/ |
H A D | Makefile | 14 PATH:=${PARSERPATH}:${PATH} macro 15 export PATH
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | ModelScript.sml | 87 (* PATH M s is true of path p iff p is a computation path of model M *) 91 `PATH M s w = 105 `COMPUTATION M w = ?s. s IN M.S0 /\ PATH M s w`;
|
H A D | UnclockedSemanticsScript.sml | 340 * PATH M s is true of p iff p is a computation path of M 356 ?p :: PATH M s. 360 ?p :: PATH M s. 367 ?p :: PATH M s.
|
H A D | ModelLemmasScript.sml | 79 ``(PATH M s (FINITE l) = 85 (PATH M s (INFINITE f) = 422 ``w IN PATH M s = PATH M s w``, 428 ``w IN COMPUTATION M = ?s. s IN M.S0 /\ PATH M s w``, 967 (PATH M s (FINITE l) = 1091 (* (PATH M (HD l) (FINITE l) = *) 1108 (PATH M (f 0) (INFINITE f) = 1133 (PATH M (ELEM w 0) w = 1247 ``PATH [all...] |
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/ |
H A D | UnclockedSemanticsScript.sml | 217 * PATH M p is true iff p is a path with respect to transition relation M.R 219 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)))`; 233 ?p. PATH M p s /\ O_SEM M f (ELEM p 1)) 236 ?p. PATH M p s /\ 240 ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`;
|
/seL4-l4v-10.1.1/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-10.1.1/graph-refine/seL4-example/ |
H A D | Makefile.common | 46 DECOMP_SCRIPT= $(shell PATH="${DECOMP_DIR}:${PATH}" sh -c "which decompile.py") 127 H4PATH=$(realpath ${HOL4_ROOT}/bin):${PATH} 132 PATH=${H4PATH} ${DECOMP_SCRIPT} --fast ./kernel --ignore=${IGNORES}
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/tools-poly/ |
H A D | smart-configure.sml | 147 case OS.Process.getEnv "PATH" of 173 else (* examine PATH variable *) 174 case OS.Process.getEnv "PATH" of 186 \to be in your PATH.\n\
|
/seL4-l4v-10.1.1/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-10.1.1/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...] |
H A D | cheney_allocScript.sml | 143 ``!xs x s t. PATH (x,xs) s /\ s SUBSET t ==> PATH (x,xs) t``, 348 \\ Q.UNDISCH_TAC `PATH (r',p ++ [x]) (apply b (ch_set h))` 382 \\ Q.UNDISCH_TAC `PATH (r',p ++ [x]) (basic_abs m)` 414 (PATH (y,p) ((x,y',z,d) INSERT s) = PATH (y,p) s)``, 417 \\ Q.UNDISCH_TAC `PATH (y,p) ((x,y',z,d) INSERT s)` 999 ``!xs x y ys. PATH (x,xs ++ y::ys) s = PATH(x,xs++[y]) s /\ PATH( [all...] |