| Thu, 15 Aug 2019 16:38:55 +0200 | wenzelm | Indexname.toString according to string_of_vname' in ML; | changeset | files |
| Thu, 15 Aug 2019 16:26:50 +0200 | wenzelm | clarified type Indexname, with plain value Int; | changeset | files |
| Thu, 15 Aug 2019 16:17:18 +0200 | wenzelm | more complete pattern match; | changeset | files |