/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | components.scala | 90 File.find_files(dir.file, 91 (file: JFile) => file.isDirectory && purge_set(file.getName),
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | isabelle_fonts.scala | 40 lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
|
/seL4-l4v-master/HOL4/tools/Holmake/tests/empty_script/ |
H A D | selftest.sml | 57 val pats = [["Couldn't find required output file:", "emptyTheory"], 58 ["Couldn't find required output file:", "noproductTheory"]]
|
/seL4-l4v-master/seL4/libsel4/tools/ |
H A D | invocation_header_gen.py | 147 help='Name of xml file with invocation definitions', required=True) 149 help='Name of file to create', required=True) 165 print("Error: invalid xml file", file=sys.stderr)
|
/seL4-l4v-master/seL4/manual/tools/libsel4_tools/ |
H A D | invocation_header_gen.py | 147 help='Name of xml file with invocation definitions', required=True) 149 help='Name of file to create', required=True) 165 print("Error: invalid xml file", file=sys.stderr)
|
/seL4-l4v-master/seL4/tools/ |
H A D | invocation_header_gen.py | 147 help='Name of xml file with invocation definitions', required=True) 149 help='Name of file to create', required=True) 165 print("Error: invalid xml file", file=sys.stderr)
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | hhExportFof.sml | 240 val file = dir ^ "/" ^ name_thm thmid ^ ".p" value 241 val oc = TextIO.openOut file 284 val file = dir ^ "/" ^ thy ^ ".ax" value 285 val oc = TextIO.openOut file 346 val file = dir ^ "/atp_in" value 347 val oc = TextIO.openOut file 366 fun fof_export_goal file (axl,cj) = 373 val oc = TextIO.openOut file
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | misc.tex | 52 As such theorems are pretty-printed into the corresponding \texttt{Theory.sig} file, the help system will find both the declaration in the signature (\eg, \ml{val~nm~:thm}), and the entry for that theorem in the comment-block. 147 text file. This file is used to achieve inter-session persistence of 148 the theory being constructed. For example, the text file resulting 157 script file; and (b) compile the resulting theory file. After this, 158 the theory file is available for use. 164 The file that generates the \HOL{} theory \textit{my}\texttt{Theory} must be called \textit{my}\texttt{Script.sml}. 174 The file \texttt{myScript.sml} should begin with the standard boilerplate: 180 This ``boilerplate'' ensures that the standard tactics and SML commands will be in the namespace when the script file i [all...] |
H A D | HolQbf.tex | 137 \paragraph{Support for the QDIMACS file format} 139 The QDIMACS standard defines an input file format for QBF solvers. 146 \ml{QDimacs.write\_qdimacs\_file path $\phi$} creates a QDIMACS file 150 variable index (a positive integer) used in the QDIMACS file. 153 file (with name \ml{path}) and returns the encoded QBF as a \HOL{} 167 {\tt /tmp} on Unix machines. The actual file names are generated at
|
/seL4-l4v-master/HOL4/Manual/Guide/ |
H A D | guide.tex | 23 \def\file{{$\langle${\it file}$\rangle$}} 24 \def\filen#1{{$\langle${\it file} #1$\rangle$}} 138 \noindent Each of these subdirectories contains a {\tt READ-ME} file explaining 166 be set by editing the style file {\tt Manual/LaTeX/layout.sty}. Near the top 167 of this file there is the declaration of a \LaTeX\ boolean flag `{\tt Afour}' 248 the \LaTeX\ source file {\tt index.tex} using the program {\tt makeindex}. 259 create the index file. One may therefore have to type {\tt make description} 364 {\tt hol/help}, a corresponding file \id\doc\ that documents it. This file i [all...] |
/seL4-l4v-master/HOL4/Manual/Tutorial/ |
H A D | intro.tex | 28 \texttt{tar} file unpacked into a directory \ml{hol}.\footnote{You may 95 A sample \texttt{LD\_LIBRARY\_PATH} initialisation command (in a file such as \texttt{.bashrc}) might be 109 - [opening file "tools/smart-configure-mosml.sml"] 163 If \texttt{smart-configure} is unable to guess correct values for the various parameters (\texttt{holdir}, \texttt{OS} \etc) then you can create a file called to provide correct values. 166 In this file, specify the correct value for the appropriate parameter by providing an ML binding for it. 178 The \texttt{config-override} file need only provide values for those 181 With this file in place, the \texttt{smart-configure} program will use 190 In extreme circumstances it is possible to edit the file 193 \texttt{tools-poly/configure.sml} instead.) At the top of this file 204 The \texttt{polymllibdir} must be a path to a directory that contains the file \textt [all...] |
/seL4-l4v-master/HOL4/polyml/ |
H A D | depcomp | 22 # distribute this file as part of a program that contains a 37 Run PROGRAMS ARGS to compile a file, generating dependencies 42 source Source file read by 'PROGRAMS ARGS'. 43 object Object file output by 'PROGRAMS ARGS'. 45 depfile Dependency file to output. 46 tmpdepfile Temporary file to use when outputting dependencies. 77 # If no dependency file was actually created by the compiler invocation, 89 # If the compiler actually managed to produce a dependency file, 137 # here, because this file can only contain one case statement. 225 # The second -e expression handles DOS-style file name [all...] |
H A D | Makefile.in | 244 # e.g., the same source file might be shared among _SOURCES variables 696 list=; while read file base inst; do \ 697 if test "$$base" = "$$inst"; then list="$$list $$file"; else \ 698 echo " $(INSTALL_DATA) '$$file' '$(DESTDIR)$(man1dir)/$$inst'"; \ 699 $(INSTALL_DATA) "$$file" "$(DESTDIR)$(man1dir)/$$inst" || exit $$?; \ 834 dist_files=`for file in $$list; do echo $$file; done | \ 842 for file in $$dist_files; do \ 843 if test -f $$file || test -d $$file; the [all...] |
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | OS.sml | 72 val splitDirFile : string -> {dir : string, file : string} 73 val joinDirFile : {dir : string, file : string} -> string 75 val file : string -> string value 119 val file : iodesc_kind value 200 is one which identifies a given file independent of any setting 474 then {dir = vol ^ separator, file = fileName} 475 else {dir = dirName, file = fileName} 479 and file s = #file(splitDirFile s) function 486 fun joinDirFile{dir, file} 942 val file : iodesc_kind = 0 value [all...] |
H A D | BinIO.sml | 70 the file descriptor itself, rather 112 (* Open a file for input. *) 119 (* Open a file for output. *)
|
/seL4-l4v-master/isabelle/src/Pure/Isar/ |
H A D | token.scala | 206 def file(file: String): Pos = new Pos(1, 1, file, "") 214 val file: String, 231 else new Pos(line1, offset1, file, id) 238 (if (file != "") Position.File(file) else Nil) :::
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Isar/ |
H A D | token.scala | 206 def file(file: String): Pos = new Pos(1, 1, file, "") 214 val file: String, 231 else new Pos(line1, offset1, file, id) 238 (if (file != "") Position.File(file) else Nil) :::
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 149 text file. This file is used to achieve inter-session persistence of 150 the theory being constructed. For example, the text file resulting 159 script file; and (b) compile the resulting theory file. After this, 160 the theory file is available for use. 169 should be added at the end of the file. When the script is finally 218 This is because (due to restrictions imposed by Moscow~ML\index{Moscow ML}) the script file is required to be an ML structure, and the contents of a structure must be \emph{declarations}, not expressions. 219 Indeed, one is allowed to (and often will) omit the bracketing \texttt{structure~foo~=~struct} - \texttt{end} lines, but the contents of the file are still interpreted as if belonging to a structure. 224 (This is on the assumption that structure \ml{Foo} is defined in a file \textt [all...] |
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | document_model.scala | 5 Document model connected to jEdit buffer or external file: content of theory 6 node or auxiliary file (blob). 121 file <- model.file if changed_files(file) 271 file <- model.file 272 } yield file.getParentFile).toSet) 279 /* file content */ 388 val file [all...] |
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Database.sml | 117 type entry = { comp : component, file : string, line : int } 121 writeString os (#file e); 130 {comp = c, file = f, line = l} 214 fun getname ({comp, file, ...} : entry) = 216 Str => file
|
H A D | Doc2Txt.sml | 142 val file = parse_file (OS.Path.concat(docdir, dname ^ ".doc")) value 145 print_docpart (file, outputstr); 146 app (write_section outputstr) file;
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | document_model.scala | 5 Document model connected to jEdit buffer or external file: content of theory 6 node or auxiliary file (blob). 121 file <- model.file if changed_files(file) 271 file <- model.file 272 } yield file.getParentFile).toSet) 279 /* file content */ 388 val file [all...] |
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SolverSpec.sml | 13 file; appends the names of input and output files to 'cmd_stem' before 15 the output file generated by the SMT solver); deletes input and output 16 file (unless '!trace' = 4); emits messages according to '!trace' *)
|
/seL4-l4v-master/HOL4/doc/hol-mode/ |
H A D | hol-mode.tex | 45 \item [l ``hol-load-file''] Loads a HOL library. If there is a region 63 \item [u ``hol-use-file''] Prompts for a file-name to be \emph{use}-d
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfLibrary.sml | 11 (* write_strings_to_file: opens 'path' as an output text file; writes all *) 12 (* elements of 'strings' to this file (in the order given); closes the *) 13 (* file *) 25 (* read_lines_from_file: opens 'path' as an input text file; reads all lines *) 26 (* of this file (using TextIO.inputLine); closes the file before *)
|