fixed comment;
authorwenzelm
Mon, 16 Dec 1996 10:01:40 +0100
changeset 2403 8115988ccc22
parent 2402 b3d273ce5601
child 2404 edcc26b1461d
fixed comment;
src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Dec 16 10:01:17 1996 +0100
+++ b/src/Pure/library.ML	Mon Dec 16 10:01:40 1996 +0100
@@ -5,7 +5,7 @@
 
 Basic library: functions, options, pairs, booleans, lists, integers,
 strings, lists as sets, association lists, generic tables, balanced trees,
-input / TextIO.output, timing, filenames, misc functions.
+input / output, timing, filenames, misc functions.
 *)
 
 infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto