/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | vscode_resources.scala | 108 val path = source_path.expand 109 if (dir == "" || path.is_absolute) File.platform_path(path) 110 else if (path.is_current) dir 111 else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator)) 112 dir + JFile.separator + File.platform_path(path) 113 else if (path.is_basic) dir + File.platform_path(path) 114 else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
H A D | modelCheck.sml | 9 (concat hol_dir "examples/PSL/path") :: 70 (*finds as counterexample the path where a always holds*) 99 (*no path, so even a contradiction holds*)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctl2muScript.sml | 65 val ELEM_REST = save_thm("ELEM_REST",prove(``!(p:'state path) (n:num). ELEM (REST p) n = ELEM p (n+1)``, 73 val PATH_REST = save_thm("PATH_REST",prove(``!(p:'state path) (M: ('prop,'state) kripke_structure) (s:'state). PATH M p s ==> PATH M (REST p) (ELEM p 1)``, 94 EXISTS_TAC ``p:'state path`` 97 EXISTS_TAC ``REST (p:'state path)`` 202 EXISTS_TAC ``INFINITE (\n. if (n=0) then s else ELEM (p':'state path) (n-1))`` 214 THEN PAT_ASSUM ``ELEM (INFINITE (f':num -> 'state)) 0 = ELEM (p:'state path) 1`` (fn t => 216 THEN PAT_ASSUM ``ELEM (p:'state path) 0 = s`` (fn t => REWRITE_TAC [SYM t]) 400 EXISTS_TAC ``p: 'state path`` 405 THEN EXISTS_TAC ``ELEM (p:'state path) 1`` 408 THEN PAT_ASSUM ``ELEM (p:'state path) [all...] |
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Net.sig | 36 of as being indexed by a path which is computed from a term which 39 one term may be indexed by the same path, i.e., the extraction 47 The term tm is used as a key to compute a path at which to 48 store x in net. If the path does not already exist in net,
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Net.sig | 36 of as being indexed by a path which is computed from a term which 39 one term may be indexed by the same path, i.e., the extraction 47 The term tm is used as a key to compute a path at which to 48 store x in net. If the path does not already exist in net,
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | selftest.sml | 6 the full path of "NuSMV" [1] executation.
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | ci_profile.scala | 75 final def hg_id(path: Path): String = 76 Mercurial.repository(path).id()
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 19 | Equality of Literal.literal * Term.path * Term.term
|
H A D | KeyMap.sml | 311 (* Generating a path by searching a tree for a key/value pair *) 313 fun treePeekPath pkey path tree = 315 E => (path,NONE) 316 | T node => nodePeekPath pkey path node 318 and nodePeekPath pkey path node = 323 LESS => treePeekPath pkey ((true,node) :: path) left 324 | EQUAL => (path, SOME node) 325 | GREATER => treePeekPath pkey ((false,node) :: path) right 328 (* A path splits a tree into left/right components *) 340 fun mkSidesPath path 395 val (path,pnode) = nodePeekPath pkey [] node value 441 val (path,inode) = treePeekPath key [] tree value [all...] |
H A D | Map.sml | 303 (* Generating a path by searching a tree for a key/value pair *) 305 fun treePeekPath compareKey pkey path tree = 307 E => (path,NONE) 308 | T node => nodePeekPath compareKey pkey path node 310 and nodePeekPath compareKey pkey path node = 315 LESS => treePeekPath compareKey pkey ((true,node) :: path) left 316 | EQUAL => (path, SOME node) 317 | GREATER => treePeekPath compareKey pkey ((false,node) :: path) right 320 (* A path splits a tree into left/right components *) 332 fun mkSidesPath path 387 val (path,pnode) = nodePeekPath compareKey pkey [] node value 433 val (path,inode) = treePeekPath compareKey key [] tree value [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | ci_profile.scala | 75 final def hg_id(path: Path): String = 76 Mercurial.repository(path).id()
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 19 | Equality of Literal.literal * Term.path * Term.term
|
H A D | KeyMap.sml | 311 (* Generating a path by searching a tree for a key/value pair *) 313 fun treePeekPath pkey path tree = 315 E => (path,NONE) 316 | T node => nodePeekPath pkey path node 318 and nodePeekPath pkey path node = 323 LESS => treePeekPath pkey ((true,node) :: path) left 324 | EQUAL => (path, SOME node) 325 | GREATER => treePeekPath pkey ((false,node) :: path) right 328 (* A path splits a tree into left/right components *) 340 fun mkSidesPath path 395 val (path,pnode) = nodePeekPath pkey [] node value 441 val (path,inode) = treePeekPath key [] tree value [all...] |
/seL4-l4v-10.1.1/HOL4/src/search/ |
H A D | dirGraphScript.sml | 63 (* path not containing p. *) 86 (* If y is reachable from x, but not z, then y is reachable from x on a path *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | bytes.scala | 91 def read(path: Path): Bytes = read(path.file) 104 def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
|
H A D | http.scala | 154 Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
|
/seL4-l4v-10.1.1/seL4/include/api/ |
H A D | debug.h | 29 switch (ksKernelEntry.path) {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | bytes.scala | 91 def read(path: Path): Bytes = read(path.file) 104 def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
|
H A D | http.scala | 154 Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
|
/seL4-l4v-10.1.1/HOL4/tools-poly/ |
H A D | smart-configure.sml | 143 (OS.Path.mkAbsolute{path = fname, relativeTo = OS.FileSys.getDir()}) 148 SOME path => 151 String.fields (fn c => c = sepc) path 162 \ val poly = \"path-to-poly\";" 171 SOME (OS.Path.mkAbsolute { path = dirify p, 229 \ val polymllibdir = \"path-to-dir-containing-libpolymain.a\";"
|
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/ |
H A D | NormalVertex.java | 17 String label="",path="",dir="",ID=""; field in class:NormalVertex 54 public String getPath() { return path;} 56 public void setPath(String p) { path=p; }
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | isabelle_tool.scala | 21 private def compile(path: Path): Body = 24 cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) 26 val source = File.read(path)
|
/seL4-l4v-10.1.1/l4v/isabelle/lib/browser/GraphBrowser/ |
H A D | NormalVertex.java | 17 String label="",path="",dir="",ID=""; field in class:NormalVertex 54 public String getPath() { return path;} 56 public void setPath(String p) { path=p; }
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | isabelle_tool.scala | 21 private def compile(path: Path): Body = 24 cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) 26 val source = File.read(path)
|
/seL4-l4v-10.1.1/HOL4/src/coalgebras/ |
H A D | pathScript.sml | 9 val _ = new_theory "path"; 12 "path", 54 val first_def = Define`first (p:('a,'b) path) = FST (fromPath p)`; 55 val stopped_at_def = Define`stopped_at x:('a,'b) path = toPath (x, LNIL)`; 57 Define`pcons x r p : ('a,'b) path = 62 ``!x y. (stopped_at x = stopped_at y : ('a,'b) path) = (x = y)``, 102 ``(!x. first (stopped_at x : ('a,'b) path) = x) /\ 103 (!x r p. first (pcons x r p : ('a,'b) path) = x)``, 107 Define`finite (sigma : ('a,'b) path) = LFINITE (SND (fromPath sigma))`; 110 ``(!x. finite (stopped_at x : ('a,'b) path) [all...] |