src/Pure/ML-Systems/polyml-old-basis.ML
2007-09-08 wenzelm 2007-09-08 added String.isSubstring;
2007-05-31 wenzelm 2007-05-31 emulate later version of TextIO.inputLine;
2007-05-31 wenzelm 2007-05-31 TextIO.inputLine: use present SML B library version;