Fri, 25 Sep 1998 14:06:00 +0200 deleted illegal "op"
paulson [Fri, 25 Sep 1998 14:06:00 +0200] rev 5567
deleted illegal "op"
Fri, 25 Sep 1998 14:05:34 +0200 uses BasisLibrary for Int.min
paulson [Fri, 25 Sep 1998 14:05:34 +0200] rev 5566
uses BasisLibrary for Int.min
Fri, 25 Sep 1998 14:05:13 +0200 patched obsolete code
paulson [Fri, 25 Sep 1998 14:05:13 +0200] rev 5565
patched obsolete code
(0) -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip