1994-05-26 ago changed use_string's type to string list -> unit because POLY can only
1994-05-19 ago added use_string: string -> unit to execute ML commands passed in a string
1993-11-09 ago fixed a bug in POLY.ML: delete_file didn't close streams;
1993-10-22 ago delete_file now has type string -> unit in both NJ and POLY,
1993-10-21 ago /NJ,POLY/delete_file: new
1993-10-15 ago file_info now returns a string that does not contain the path/filename
1993-10-04 ago Pure/ROOT.ML
1993-09-16 ago Initial revision