Thu, 23 Feb 2023 16:17:04 +0000 paulson has_sum now an infix operator!!
Thu, 23 Feb 2023 15:21:22 +0000 paulson merged
Thu, 23 Feb 2023 15:21:14 +0000 paulson New material contributed by Manuel
Thu, 23 Feb 2023 22:04:32 +0100 nipkow Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 tip