/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryReader.sml | 253 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 D | ctlScript.sml | 96 * 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 D | configure-mosml.sml | 113 (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 D | make_iss.sml | 25 (itstrings (fn chunk => fn path => Path.concat (chunk,path)) slist);
|
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/ |
H A D | GraphBrowser.java | 57 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 D | TreeNode.java | 19 String name,path; field in class:TreeNode 57 path=p;
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | scala_console.scala | 37 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 D | GraphBrowser.java | 57 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 D | TreeNode.java | 19 String name,path; field in class:TreeNode 57 path=p;
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | scala_console.scala | 37 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 D | isa-common.mk | 17 # Get path to the base of the repository.
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | check.py | 319 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 D | process_env.cpp | 215 // 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 D | thy_resources.scala | 85 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 D | thy_resources.scala | 85 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 D | parse_doxygen_xml.py | 506 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 D | ltmain.sh | 184 # 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 D | ltmain.sh | 184 # 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 D | PSLPathScript.sml | 52 * 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 D | Induction.sml | 153 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 D | build.scala | 302 (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 D | build.scala | 302 (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 D | SolverSpec.sml | 72 List.app (fn path => OS.FileSys.remove path handle SysErr _ => ())
|
H A D | Z3.sml | 15 fun is_sat_file path = 17 val instream = TextIO.openIn path
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttExtract.sml | 51 val path = #file (hd decll) value 53 path
|