/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | metis.sml | 207 TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n"); 238 TextIO.print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n"); 280 ("\nSZS output start Saturation for " ^ filename ^ "\n") 286 ("SZS output end Saturation for " ^ filename ^ "\n\n")
|
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser1.sml | 12 val print = fn s => output(std_out,s)
|
/seL4-l4v-master/HOL4/src/AI/machine_learning/ |
H A D | mlMatrix.sml | 97 Input/output
|
H A D | mlNeuralNetwork.sig | 49 (* input/output *)
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | keymap_merge.scala | 106 if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" 109 HTML.output("--- " + shortcut.toString) +
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | keymap_merge.scala | 106 if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>" 109 HTML.output("--- " + shortcut.toString) +
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Library.sml | 13 0 - no output at all (except for fatal errors) 28 (* opens 'path' as an output text file; writes all elements of 34 List.app (TextIO.output o Lib.pair outstream) strings;
|
/seL4-l4v-master/HOL4/developers/ |
H A D | comparelogs.sml | 10 fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 27 \ -q Print raw data only, no sums, or fancy lines; (output to other tools)\n\ 176 output a map from theory-names to average times
|
/seL4-l4v-master/HOL4/examples/RL_Environment/ |
H A D | RL_Environment.sml | 174 (TextIO.output(TextIO.stdOut, String.concat[name," : Reinforcement Learning environment for HOL4\n\n"]); 175 TextIO.output(TextIO.stdOut, String.concat["Arguments: \n"]); 176 TextIO.output(TextIO.stdOut, arguments_help);
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Doc2Html.sml | 26 fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 86 let fun outss ss = TextIO.output(ostrm, Substring.translate encode ss) 87 fun out s = TextIO.output(ostrm,s)
|
H A D | Doc2Tex.sml | 10 fun warn s = TextIO.output(TextIO.stdErr, s ^ "\n") 11 fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 13 fun out(str,s) = TextIO.output(str, s)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | ImperativeIO.sml | 43 (* An imperative output stream is a reference to the underlying stream. 159 fun output(out, v) = StreamIO.output(getOutstream out, v) function
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Lib.sml | 233 fun x64_test_aux i input output = let 262 val output2 = filter (fn (x,y) => not (mem x xs)) output 263 val output1 = filter (fn (x,y) => mem x xs) output 286 val output = map get_output diff value 289 val th = SOME (x64_test_aux i input output) handle e => NONE
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 216 You should get the following output: 301 By just looking at Nitpick's output, it might not be clear why the 643 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$. 849 Nitpick's output is very instructive. First, it tells us that the predicate is 854 The output also shows how each iteration contributes to $\textit{even}'$. The 890 Notice the special constraint $\textit{even}' \leq \ldots$ in the output, whose 940 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and 1164 An interesting aspect of Nitpick's verbose output is that it assigned inceasing 1682 Nitpick's output reveals that the element $0$ was added as a left child of $1$, 1737 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output [all...] |
/seL4-l4v-master/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 216 You should get the following output: 301 By just looking at Nitpick's output, it might not be clear why the 643 In the output above, $\Abs{n}$ abbreviates $\textit{Abs\_three}~n$. 849 Nitpick's output is very instructive. First, it tells us that the predicate is 854 The output also shows how each iteration contributes to $\textit{even}'$. The 890 Notice the special constraint $\textit{even}' \leq \ldots$ in the output, whose 940 In the output, $\textit{odd}_{\textrm{base}}$ represents the base elements and 1164 An interesting aspect of Nitpick's verbose output is that it assigned inceasing 1682 Nitpick's output reveals that the element $0$ was added as a left child of $1$, 1737 (\S\ref{mode-of-operation}), scope of search (\S\ref{scope-of-search}), output [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 647 val _ = map (fn s => TextIO.output(file_st, s^"\n")) 649 val _ = TextIO.output(file_st, "\n\n"); 658 val _ = map (fn s => TextIO.output(file_st, s^"\n")) 660 val _ = TextIO.output(file_st, "\n\n"); 668 val _ = map (fn s => TextIO.output(file_st, s^"\n")) 670 val _ = TextIO.output(file_st, "\n\n");
|
/seL4-l4v-master/HOL4/tools/ |
H A D | configure.sml | 109 then TextIO.output(ostrm, residue) 110 else (TextIO.output(ostrm, line); loop()) 122 output(ostrm, inputAll istrm); 140 else (BinIO.output(outstr, v); loop()) 235 fun echo s = (TextIO.output(TextIO.stdOut, s^"\n"); 500 BinIO.output(ostrm, v);
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | file.scala | 190 val output = new StringBuilder(100) 192 while ({ c = reader.read; c != -1 }) output += c.toChar 194 output.toString
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | file.scala | 190 val output = new StringBuilder(100) 192 while ({ c = reader.read; c != -1 }) output += c.toChar 194 output.toString
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | Feedback.sml | 65 fun out strm s = (TextIO.output(strm, s); TextIO.flushOut strm) 75 * Formatting and output for exceptions, messages, and warnings. * 154 * Traces, numeric flags; the higher setting, the more verbose the output. *
|
/seL4-l4v-master/HOL4/examples/dev/Fact32/ |
H A D | exor32.ml | 62 \ output [size:0] out;\n\
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Stream.sml | 181 | to_file (CONS (x,y)) = (output (h,x); to_file (y ()))
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | SatSolvers.sml | 12 ** post_run, (* transform SAT solver output before reading into HOL *)
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | inttoScript.sml | 27 (* store_thm or as prove, thus maximizing or minimizing the output *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibStream.sml | 160 | to_file (CONS (x,y)) = (output (h,x); to_file (y ()))
|