| Sun, 15 Mar 2015 12:49:20 +0100 | wenzelm | more command categories, as in ML; | changeset | files |
| Sun, 15 Mar 2015 12:42:30 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 14 Mar 2015 21:16:29 +0100 | wenzelm | value-oriented user error, for well-defined Thy_Syntax.chop_common; | changeset | files |
| Sat, 14 Mar 2015 20:49:10 +0100 | wenzelm | more explicit exception User_Error, with value-oriented equality; | changeset | files |