Searched refs:path (Results 126 - 150 of 367) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/
H A Dvscode_resources.scala108 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 DmodelCheck.sml9 (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 Dctl2muScript.sml65 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 DNet.sig36 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 DNet.sig36 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 Dselftest.sml6 the full path of "NuSMV" [1] executation.
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/
H A Dci_profile.scala75 final def hg_id(path: Path): String =
76 Mercurial.repository(path).id()
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DProof.sig19 | Equality of Literal.literal * Term.path * Term.term
H A DKeyMap.sml311 (* 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 DMap.sml303 (* 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 Dci_profile.scala75 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 DProof.sig19 | Equality of Literal.literal * Term.path * Term.term
H A DKeyMap.sml311 (* 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 DdirGraphScript.sml63 (* 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 Dbytes.scala91 def read(path: Path): Bytes = read(path.file)
104 def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
H A Dhttp.scala154 Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
/seL4-l4v-10.1.1/seL4/include/api/
H A Ddebug.h29 switch (ksKernelEntry.path) {
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dbytes.scala91 def read(path: Path): Bytes = read(path.file)
104 def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
H A Dhttp.scala154 Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
/seL4-l4v-10.1.1/HOL4/tools-poly/
H A Dsmart-configure.sml143 (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 DNormalVertex.java17 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 Disabelle_tool.scala21 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 DNormalVertex.java17 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 Disabelle_tool.scala21 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 DpathScript.sml9 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...]

Completed in 323 milliseconds

1234567891011>>