Fri, 18 Apr 1997 11:54:54 +0200 paulson Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
Fri, 18 Apr 1997 11:53:55 +0200 paulson Now loads theory LList indirectly: via LFilter
Fri, 18 Apr 1997 11:53:16 +0200 paulson Now uses some "case" syntax (but could use more)
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip