Fri, 14 Jun 2019 08:34:27 +0000 | haftmann | removed relics of ASCII syntax for indexed big operators | changeset | files |
Fri, 14 Jun 2019 08:34:27 +0000 | haftmann | dropped former legacy input abbreviations | changeset | files |
Fri, 14 Jun 2019 08:34:27 +0000 | haftmann | using (*)-syntax for partially applied infix is fine, contrary to ancient op-syntax | changeset | files |