author | wenzelm |
Mon, 16 Dec 1996 10:01:40 +0100 | |
changeset 2403 | 8115988ccc22 |
parent 2402 | b3d273ce5601 |
child 2404 | edcc26b1461d |
--- 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