Thu, 23 Feb 2023 16:17:04 +0000 | paulson | has_sum now an infix operator!! | changeset | files |
Thu, 23 Feb 2023 15:21:22 +0000 | paulson | merged | changeset | files |
Thu, 23 Feb 2023 15:21:14 +0000 | paulson | New material contributed by Manuel | changeset | files |
Thu, 23 Feb 2023 22:04:32 +0100 | nipkow | Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation | changeset | files |