/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | FinalPolyML.sml | 37 The rootFunction has now been pulled out into a separate file and is added on 163 location is the file-name, line number and position. context is an 174 the current file, a byte offset or simply zero. 177 (* The current file being compiled. This is used by the default CPErrorMessageProc 277 SOME (ContextLocation{file,startLine,startPosition,endPosition, ...}) => 280 file name convert it to ESC-ESC. *) 285 stream(String.translate escapeEscapes file); 414 location={startLine, startPosition, endPosition, file, ...}: PolyML.location, 440 file, (* TODO double any escapes. *) separator, 452 ( (if file [all...] |
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | SatSolvers.sml | 2 ** This file contains specifications of the SAT tools that 10 ** notime_run, (* command to invoke solver on a file *) 11 ** time_run, (* command to invoke on a file and time *)
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | intro.tex | 30 file \texttt{tar} sia stato estratto in una directory \ml{hol}\footnote{Si pu� 46 {\tt sigobj} & Directory per i file object \ML{} & Directory\\ 96 Se questi file sono in \texttt{/usr/lib}, non c'� bisogno di cambiare nulla, ma altre posizioni possono richiedere un'ulteriore configurazione di sistema. 97 Un esempio di comando di inizializzazione di \texttt{LD\_LIBRARY\_PATH} (in un file come \texttt{.bashrc}) potrebbe essere 110 - [opening file "tools/smart-configure-mosml.sml"] 162 creare un file richiamato per fornire i valori corretti. Con Moscow~ML, questo 165 nella directory \texttt{tools-poly}. In questo file, si specifichi il 179 Il file \texttt{config-override} ha bisogno di fornire soli i valori per quelle 182 Con questo file nel posto corretto, il programma \texttt{smart-configure} user� 191 In circostanze estreme � possibile modificare il file [all...] |
H A D | more-examples.tex | 37 con il suo sistema di tipi. I file furono sviluppati originariamente da Tom Melham 47 Questo file illustra l'implementazione di John Harrison di 62 Questa sotto directory contiene i file usati nell'esempio di parit� del
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | MyDatabase.sml | 16 type entry = { comp : component, file : string, line : int } 81 fun getname ({comp, file, ...} : entry) = 83 Str => file
|
H A D | Database.sig | 13 type entry = { comp : component, file : string, line : int }
|
H A D | MyDatabase-sig.sml | 16 type entry = { comp : component, file : string, line : int }
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/Examples/ |
H A D | mlEdit.sml | 173 file = "", 184 | SOME {file, ...} => 189 val f = TextIO.openIn file 195 (* Should we save any existing file? *) 200 fileName=file}) 203 SOME(concat["Unable to open - ", file, "\n"(*, exnMessage exn*)]), 210 then (* Save to the original file name if there is one. *) 222 (LRESINT 0, (* Use the selected file name. *) 503 (* Write the document to the given file name. *) 505 (* Write the file a [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | gr.sml | 4 * COPYRIGHT (c) 1997 by Martin Erwig. See COPYRIGHT file for details.
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr.sml | 4 * COPYRIGHT (c) 1997 by Martin Erwig. See COPYRIGHT file for details.
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr.sml | 4 * COPYRIGHT (c) 1997 by Martin Erwig. See COPYRIGHT file for details.
|
/seL4-l4v-master/HOL4/src/opentheory/postbool/ |
H A D | OpenTheoryIO.sml | 44 val t = Curl.submitFile {url=url,field="article",file=t}
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | PIntMap.sig | 14 * (enclosed in the file LGPL).
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | mkroot.scala | 36 if (root_path.file.exists) error("Cannot overwrite existing " + root_path) 39 if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
|
/seL4-l4v-master/HOL4/polyml/Tests/ |
H A D | RunTests.sml | 13 (* Run a file. Returns true if it succeeds, false if it fails. *) 111 val testPath = joinDirFile{dir=parentDir, file=dirName} 146 if runTest(joinDirFile{dir=testPath, file=f}) 148 else (print "Failed!!\n"; runDir(files, fails @ [joinDirFile{dir=dirName, file=f}]))
|
/seL4-l4v-master/HOL4/examples/ |
H A D | tempScript.sml | 5 * for theory "x", you must change the name of this file to "xScript.sml", *
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | mkroot.scala | 36 if (root_path.file.exists) error("Cannot overwrite existing " + root_path) 39 if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | DiskThms.sml | 31 | _ => raise Fail "Couldn't parse sexp from file"
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindex.sml | 14 (* Parse the input file *) 19 val file = "/home/tt291/Documents/thesis/holmunge/test.hix"; 103 | ["Overrides", file] => 104 (mungeTools.user_overrides := mungeTools.read_overrides file; 122 val file = if Path.isAbsolute filename then filename else value 124 val entryL = AssembleHolindexParser.parse_hdf_file file; 155 fun parse_hix file = 158 val fh = Portable.open_in file; 159 val basedir = Path.dir file; 540 val file [all...] |
H A D | holindex-demo.tex | 19 \setHOLoverrides{file} %optional 91 Definitions like these inside a latex file are tedious, 93 an external file for all these definitions. There 103 label = "a short description of term form external file", 110 label = "a short description of the type from external file", 146 %use external file 246 line to the header of your file: 255 definitions are printed. Just copy them to the header of your file
|
/seL4-l4v-master/HOL4/examples/HolBdd/ |
H A D | Varmap.sml | 11 (* Thu Oct 4 15:45:52 BST 2001 -- created file *) 13 (* Thu Mar 28 09:40:05 GMT 2002 -- added signature file *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | DragDrop.sml | 41 (* Call DragQueryFile to get the file(s). *) 65 (* Call DragQueryPoint to find out where to drop the file(s). *)
|
/seL4-l4v-master/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/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/examples/separationLogic/src/holfoot/ |
H A D | selftest.sml | 27 fun test_file file = let 29 val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) []));
|