| Thu, 11 Apr 2019 15:26:19 +0100 | paulson | merged | changeset | files |
| Thu, 11 Apr 2019 15:26:04 +0100 | paulson | type instantiations for poly_mapping as a real_normed_vector | changeset | files |
| Thu, 11 Apr 2019 17:07:52 +0200 | wenzelm | visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937); | changeset | files |
| Thu, 11 Apr 2019 16:51:44 +0200 | wenzelm | tuned signature according to ML version; | changeset | files |