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