| Thu, 17 Mar 2016 16:56:44 +0100 | wenzelm | @{make_string} is available during Pure bootstrap; | changeset | files |
| Thu, 17 Mar 2016 13:44:18 +0100 | wenzelm | clarified modules; | changeset | files |
| Thu, 17 Mar 2016 12:32:12 +0100 | wenzelm | unused; | changeset | files |
| Thu, 17 Mar 2016 10:54:28 +0100 | wenzelm | hide critical structures of Poly/ML, to make it harder to disrupt the ML environment; | changeset | files |
| Thu, 17 Mar 2016 10:22:50 +0100 | wenzelm | obsolete; | changeset | files |
| Thu, 17 Mar 2016 10:21:43 +0100 | wenzelm | tuned signature; | changeset | files |