| changeset 26513 | 6f306c8c2c54 |
| parent 26500 | b4f0f36a28da |
| child 26562 | 9d25ef112cf6 |
--- a/NEWS Wed Apr 02 15:58:31 2008 +0200 +++ b/NEWS Wed Apr 02 15:58:32 2008 +0200 @@ -57,6 +57,8 @@ *** HOL *** +* Explicit class "eq" for executable equality. INCOMPATIBILITY. + * Class finite no longer treats UNIV as class parameter. Use class enum from theory Library/Enum instead to achieve a similar effect. INCOMPATIBILITY.