src/Pure/POLY.ML
Tue, 09 Nov 1993 14:24:45 +0100 clasohm fixed a bug in POLY.ML: delete_file didn't close streams;
Fri, 22 Oct 1993 13:39:23 +0100 clasohm delete_file now has type string -> unit in both NJ and POLY,
Thu, 21 Oct 1993 17:10:15 +0100 lcp /NJ,POLY/delete_file: new
Fri, 15 Oct 1993 12:51:21 +0100 clasohm file_info now returns a string that does not contain the path/filename
Mon, 04 Oct 1993 15:36:31 +0100 wenzelm Pure/ROOT.ML
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip