Fri, 10 Oct 1997 14:51:58 +0200 wenzelm tuned;
Thu, 09 Oct 1997 18:01:27 +0200 wenzelm \n at end;
Thu, 09 Oct 1997 17:45:03 +0200 wenzelm ensure that dots in formulas are followed by non-idents;
Thu, 09 Oct 1997 17:20:15 +0200 wenzelm *** empty log message ***
Thu, 09 Oct 1997 15:06:49 +0200 wenzelm no longer handles consts "" -- use syntax instead;
Thu, 09 Oct 1997 15:04:21 +0200 wenzelm removed open;
(0) -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip