src/Pure/Thy/browser_info.ML
Fri, 10 Oct 1997 15:51:38 +0200 wenzelm BAD_space_explode;
Tue, 30 Sep 1997 12:53:54 +0200 berghofe Changed html data directory and names of graph files.
Thu, 07 Aug 1997 23:43:30 +0200 berghofe Modified graph data directory.
Wed, 06 Aug 1997 14:12:29 +0200 wenzelm tuned copy_file;
Wed, 06 Aug 1997 00:24:49 +0200 berghofe This file now contains all functions for generating html
less more (0) tip