| Wed, 17 May 2017 13:50:30 +0200 | wenzelm | eliminated unused operations; | changeset | files |
| Wed, 17 May 2017 13:47:19 +0200 | wenzelm | tuned signature; | changeset | files |
| Wed, 17 May 2017 11:53:16 +0200 | wenzelm | clarified universal table: include ml_statistics; | changeset | files |