Lines Matching refs:output
80 fun output s = TextIO.output(ostrm, s)
85 output "@echo off\n";
86 output "rem The bare HOL script\n";
87 output "rem (automatically generated by HOL configuration)\n\n";
88 output (String.concat["call ", mosml, " -P full -I ", sigobj, " ",
97 fun output s = TextIO.output(ostrm, s)
104 output "@echo off\n";
105 output "rem The HOL script (with quote preprocessing)\n";
106 output "rem (automatically generated by HOL configuration)\n\n";
107 output (String.concat ["call ", qfilter, " | ", mosml,