src/Pure/library.ML
changeset 2403 8115988ccc22
parent 2317 672015b535d7
child 2471 09634c9cbf3c
--- 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