Fri, 18 Aug 1995 15:20:02 +0200 clarified comment
paulson [Fri, 18 Aug 1995 15:20:02 +0200] rev 1231
clarified comment
Fri, 18 Aug 1995 12:28:02 +0200 fixed bug in findI
nipkow [Fri, 18 Aug 1995 12:28:02 +0200] rev 1230
fixed bug in findI removed duplicates in findEs
Thu, 17 Aug 1995 15:07:09 +0200 deactivated fix_shyps.
nipkow [Thu, 17 Aug 1995 15:07:09 +0200] rev 1229
deactivated fix_shyps.
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip