Fri, 21 Oct 2005 16:34:22 +0200 added simplified settings for Poly/ML 4.x (commented out);
wenzelm [Fri, 21 Oct 2005 16:34:22 +0200] rev 17954
added simplified settings for Poly/ML 4.x (commented out);
Fri, 21 Oct 2005 16:22:59 +0200 reverted (accidental?) change of 1.148;
wenzelm [Fri, 21 Oct 2005 16:22:59 +0200] rev 17953
reverted (accidental?) change of 1.148;
Fri, 21 Oct 2005 14:49:49 +0200 abandoned rational number functions in favor of General/rat.ML
haftmann [Fri, 21 Oct 2005 14:49:49 +0200] rev 17952
abandoned rational number functions in favor of General/rat.ML
Fri, 21 Oct 2005 14:49:04 +0200 introduced functions from Pure/General/rat.ML
haftmann [Fri, 21 Oct 2005 14:49:04 +0200] rev 17951
introduced functions from Pure/General/rat.ML
Fri, 21 Oct 2005 14:47:37 +0200 slight corrections
haftmann [Fri, 21 Oct 2005 14:47:37 +0200] rev 17950
slight corrections
Fri, 21 Oct 2005 10:32:59 +0200 substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:32:59 +0200] rev 17949
substantially improved integration of website into distribution framework
Fri, 21 Oct 2005 10:32:04 +0200 substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:32:04 +0200] rev 17948
substantially improved integration of website into distribution framework
Fri, 21 Oct 2005 10:27:02 +0200 substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:27:02 +0200] rev 17947
substantially improved integration of website into distribution framework
Fri, 21 Oct 2005 10:21:38 +0200 substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:21:38 +0200] rev 17946
substantially improved integration of website into distribution framework
Fri, 21 Oct 2005 09:54:03 +0200 towards an improved website/makedist integration
haftmann [Fri, 21 Oct 2005 09:54:03 +0200] rev 17945
towards an improved website/makedist integration
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip