src/Pure/ML-Systems/polyml-5.0.ML
Sun, 16 Sep 2007 14:55:48 +0200 wenzelm use_text/file: tune text (cf. ML_Parse.fix_ints);
Thu, 31 May 2007 01:25:24 +0200 wenzelm TextIO.inputLine: use present SML B library version;
Sun, 21 Jan 2007 16:43:42 +0100 wenzelm use_text: added name argument;
Fri, 29 Dec 2006 03:57:01 +0100 wenzelm use_ml: reverted to simple output (Poly/ML changed);
Thu, 14 Dec 2006 21:46:59 +0100 wenzelm activated improved use_ml, which captures output and reports source positions;
Mon, 11 Dec 2006 19:05:25 +0100 wenzelm added improved versions of use_text/file (still inactive);
Tue, 05 Dec 2006 18:33:29 +0100 wenzelm setup for polyml-5.0;
less more (0) tip