Lines Matching defs:output
132 fun output s = TextIO.output(ostrm, s)
134 output "#!/bin/sh\n";
135 output "# The bare HOL script\n";
136 output "# (automatically generated by HOL configuration)\n\n";
137 output (fullPath [HOLDIR, "bin", "buildheap"] ^
146 fun output s = TextIO.output(ostrm, s)
152 output "#!/bin/sh\n";
153 output "# The HOL script (with quote preprocessing)\n";
154 output "# (automatically generated by HOL configuration)\n\n";
155 output (String.concatWith " "