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 |