Searched refs:output (Results 201 - 225 of 488) sorted by relevance

1234567891011>>

/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A Dmetis.sml207 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 Dparser1.sml12 val print = fn s => output(std_out,s)
/seL4-l4v-master/HOL4/src/AI/machine_learning/
H A DmlMatrix.sml97 Input/output
H A DmlNeuralNetwork.sig49 (* input/output *)
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dkeymap_merge.scala106 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 Dkeymap_merge.scala106 if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
109 HTML.output("--- " + shortcut.toString) +
/seL4-l4v-master/HOL4/src/HolSmt/
H A DLibrary.sml13 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 Dcomparelogs.sml10 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 DRL_Environment.sml174 (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 DDoc2Html.sml26 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 DDoc2Tex.sml10 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 DImperativeIO.sml43 (* 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 Dx64_Lib.sml233 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 Droot.tex216 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 Droot.tex216 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 Dc_outputLib.sml647 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 Dconfigure.sml109 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 Dfile.scala190 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 Dfile.scala190 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 DFeedback.sml65 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 Dexor32.ml62 \ output [size:0] out;\n\
/seL4-l4v-master/HOL4/examples/elliptic/
H A DStream.sml181 | to_file (CONS (x,y)) = (output (h,x); to_file (y ()))
/seL4-l4v-master/HOL4/src/HolSat/
H A DSatSolvers.sml12 ** post_run, (* transform SAT solver output before reading into HOL *)
/seL4-l4v-master/HOL4/src/integer/
H A DinttoScript.sml27 (* store_thm or as prove, thus maximizing or minimizing the output *)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibStream.sml160 | to_file (CONS (x,y)) = (output (h,x); to_file (y ()))

Completed in 110 milliseconds

1234567891011>>