Thu, 08 Nov 2018 14:48:20 +0100 | wenzelm | clarified ML positions (see also 1a52baa70aed); | changeset | files |
Thu, 08 Nov 2018 13:42:36 +0100 | wenzelm | more standard Resources.provide_parse_files: avoid duplicate markup reports; | changeset | files |
Thu, 08 Nov 2018 12:32:06 +0100 | wenzelm | more uniform (see 1722cc56d22e); | changeset | files |
Thu, 08 Nov 2018 09:11:52 +0100 | haftmann | removed relics of ASCII syntax for indexed big operators | changeset | files |
Wed, 07 Nov 2018 23:03:45 +0100 | wenzelm | tuned; | changeset | files |
Wed, 07 Nov 2018 22:38:38 +0100 | wenzelm | obsolete; | changeset | files |