| Sat, 09 Jan 2016 22:22:17 +0100 | wenzelm | generate HTML version of NEWS, with proper symbol rendering; | changeset | files |
| Sat, 09 Jan 2016 22:00:22 +0100 | wenzelm | tuned -- according to ML version; | changeset | files |
| Sat, 09 Jan 2016 20:56:00 +0100 | wenzelm | suppress somewhat pointless description (NB: this is displayed in 'print_methods'); | changeset | files |
| Sat, 09 Jan 2016 13:31:31 +0100 | wenzelm | merged | changeset | files |
| Sat, 09 Jan 2016 13:31:17 +0100 | wenzelm | tuned syntax; | changeset | files |
| Sat, 09 Jan 2016 13:00:04 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 09 Jan 2016 12:58:57 +0100 | wenzelm | \<struct> loses its rendering and is superseded by \<diamondop>; | changeset | files |