Fri, 01 Dec 2006 16:08:45 +0100 Added missing "standard"
nipkow [Fri, 01 Dec 2006 16:08:45 +0100] rev 21618
Added missing "standard"
Fri, 01 Dec 2006 12:23:53 +0100 Deleted dead code
paulson [Fri, 01 Dec 2006 12:23:53 +0100] rev 21617
Deleted dead code
(0) -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip