Searched refs:file (Results 226 - 250 of 645) sorted by relevance

1234567891011>>

/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dcomponents.scala90 File.find_files(dir.file,
91 (file: JFile) => file.isDirectory && purge_set(file.getName),
/seL4-l4v-master/l4v/isabelle/src/Pure/System/
H A Disabelle_fonts.scala40 lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
/seL4-l4v-master/HOL4/tools/Holmake/tests/empty_script/
H A Dselftest.sml57 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 Dinvocation_header_gen.py147 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 Dinvocation_header_gen.py147 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 Dinvocation_header_gen.py147 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 DhhExportFof.sml240 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 Dmisc.tex52 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 DHolQbf.tex137 \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 Dguide.tex23 \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 Dintro.tex28 \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 Ddepcomp22 # 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 DMakefile.in244 # 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 DOS.sml72 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 DBinIO.sml70 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 Dtoken.scala206 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 Dtoken.scala206 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 Dmisc.tex149 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 Ddocument_model.scala5 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 DDatabase.sml117 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 DDoc2Txt.sml142 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 Ddocument_model.scala5 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 DSolverSpec.sml13 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 Dhol-mode.tex45 \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 DQbfLibrary.sml11 (* 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 *)

Completed in 120 milliseconds

1234567891011>>