Searched refs:path (Results 176 - 200 of 367) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheoryReader.sml253 fun read_thydata path =
255 val file = TextIO.openIn path
268 fun load_thydata thyname path =
270 val l0 = H "read_thydata" read_thydata path
/seL4-l4v-10.1.1/HOL4/src/tfl/examples/
H A DctlScript.sml96 * CTL* restricted st X, FU, G, U and R are preceded by a path quantifier
97 * ie path formulae are restricted st
98 * if f and g are state formulae then Xf FUf Gf fUg and fRg are path formulae
126 * A2) no E path quantifier (only A)
/seL4-l4v-10.1.1/HOL4/tools/
H A Dconfigure-mosml.sml113 (OS.Path.mkAbsolute{path = fname, relativeTo = OS.FileSys.getDir()})
118 SOME path =>
121 String.fields (fn c => c = sepc) path
175 SOME (Path.mkAbsolute {path = dirify p,
H A Dmake_iss.sml25 (itstrings (fn chunk => fn path => Path.concat (chunk,path)) slist);
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/
H A DGraphBrowser.java57 String path = gfname.substring(0, gfname.lastIndexOf('/') + 1);
65 rd = new FileReader(path + fname);
167 System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
H A DTreeNode.java19 String name,path; field in class:TreeNode
57 path=p;
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Dscala_console.scala37 space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
39 val path =
43 path.mkString(JFile.pathSeparator)
/seL4-l4v-10.1.1/l4v/isabelle/lib/browser/GraphBrowser/
H A DGraphBrowser.java57 String path = gfname.substring(0, gfname.lastIndexOf('/') + 1);
65 rd = new FileReader(path + fname);
167 System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
H A DTreeNode.java19 String name,path; field in class:TreeNode
57 path=p;
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Dscala_console.scala37 space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
39 val path =
43 path.mkString(JFile.pathSeparator)
/seL4-l4v-10.1.1/l4v/misc/
H A Disa-common.mk17 # Get path to the base of the repository.
/seL4-l4v-10.1.1/graph-refine/
H A Dcheck.py319 def proof_subproblems (p, kind, args, restrs, hyps, path):
327 '%s (%d limited)' % (path, args[0]))]
330 return [(restrs, hyps + [hyp], path)]
334 '%d init case in %s' % (split[0][0], path)),
336 '%d loop case in %s' % (split[0][0], path))]
343 'true case (%d visited) in %s' % (point, path)),
345 'false case (%d not visited) in %s' % (point, path))]
697 return [(hyps + [ret_eq], nlerr_pc, 'Leaf path-cond imp')] + checks
702 def proof_checks_imm (p, restrs, hyps, proof, path):
716 return [(hs, hyp, '%s on %s' % (name, path))
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dprocess_env.cpp215 // spawnvp does any necessary path searching if argv[0]
216 // does not contain a full path.
379 case 11: /* Match the volume name part of a path. */
384 PolyWord path = args->Word(); local
395 TempString buff(path);
402 /* Absolute path. */
436 if (IS_INT(path)) toTest = UNTAGGED(path);
438 PolyStringObject * ps = (PolyStringObject *)path.AsObjPtr();
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dthy_resources.scala85 val tmp_dir_name: String = File.path(tmp_dir).implode
288 val path = node_name.path
289 if (!node_name.is_theory) error("Not a theory file: " + path)
292 val text = File.read(path)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/
H A Dthy_resources.scala85 val tmp_dir_name: String = File.path(tmp_dir).implode
288 val path = node_name.path
289 if (!node_name.is_theory) error("Not a theory file: " + path)
292 val text = File.read(path)
/seL4-l4v-10.1.1/seL4/manual/tools/
H A Dparse_doxygen_xml.py506 Takes a path to a file containing doxygen-generated xml,
511 dir_name = os.path.dirname(input_file_name)
526 new_input_file = os.path.join(dir_name, new_input_file_name)
562 if not os.path.exists(os.path.dirname(args.output)):
563 os.makedirs(os.path.dirname(args.output))
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dltmain.sh184 # CHECK_FUNC should accept the path to a candidate program, and
226 # Unless the user overrides by setting SED, search the path for either GNU
268 # Unless the user overrides by setting GREP, search the path for either GNU
342 # Sed substitution that converts a w32 file name or path
839 # Make sure the entire path to DIRECTORY-PATH is available.
857 # list incase some portion of path contains whitespace.
925 # Remove doubled-up and trailing slashes, "." path components,
926 # and cancel out any ".." path components in PATH after making
927 # it an absolute path.
932 # These SED scripts presuppose an absolute path wit
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/
H A Dltmain.sh184 # CHECK_FUNC should accept the path to a candidate program, and
226 # Unless the user overrides by setting SED, search the path for either GNU
268 # Unless the user overrides by setting GREP, search the path for either GNU
342 # Sed substitution that converts a w32 file name or path
839 # Make sure the entire path to DIRECTORY-PATH is available.
857 # list incase some portion of path contains whitespace.
925 # Remove doubled-up and trailing slashes, "." path components,
926 # and cancel out any ".." path components in PATH after making
927 # it an absolute path.
932 # These SED scripts presuppose an absolute path wit
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/path/
H A DPSLPathScript.sml52 * A path is finite or infinite
56 `path = FINITE of ('s list)
160 `xnum = INFINITY (* length of an infinite path *)
161 | XNUM of num`; (* length of a finite path *)
643 * CAT(w,p) creates a new path by concatenating w in front of p
733 ``!(w:'a path) i (w':'a path). ELEM (CAT (SEL w (0,i),w')) 0 = ELEM w 0``,
782 THEN IMP_RES_TAC(ISPEC ``p :'a path`` SEL_SPLIT)
802 (ISPECL [``p :'a path``,``j:num-1``,``i:num``,``j:num``] SEL_SPLIT)
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DInduction.sml153 val org_in = {path=[z], rows=rows}
156 val in_2 = {path=rstp, rows=zip pat_rectangle' rights'}
161 val {path=u::rstp, rows as (p::_, _)::_} = in_3
163 val {path=u::rstp, rows as (p::_, _)::_} = {path=rstp, rows=zip pat_rectangle' rights'}
168 hm = mk_case ty_info FV thy {path=[z], rows=rows}
170 val arg0 = {path=[z], rows=rows}
171 val {path=rstp0, rows = rows0} = el 1 news
196 | mk{path=[], rows = [([], (thm, bindings))]} = IT_EXISTS bindings thm
197 | mk{path
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dbuild.scala302 (args, path) <-
305 val body = Bytes.read(path)
306 path.file.delete
475 (path, _) <- base.sources.iterator
476 } yield path).toList
480 filterNot(path => exclude_files.contains(path.canonical_file))
483 unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dbuild.scala302 (args, path) <-
305 val body = Bytes.read(path)
306 path.file.delete
475 (path, _) <- base.sources.iterator
476 } yield path).toList
480 filterNot(path => exclude_files.contains(path.canonical_file))
483 unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSolverSpec.sml72 List.app (fn path => OS.FileSys.remove path handle SysErr _ => ())
H A DZ3.sml15 fun is_sat_file path =
17 val instream = TextIO.openIn path
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttExtract.sml51 val path = #file (hd decll) value
53 path

Completed in 346 milliseconds

1234567891011>>