1.1 --- a/NEWS Fri Apr 23 10:50:17 2010 +0200
1.2 +++ b/NEWS Fri Apr 23 13:58:14 2010 +0200
1.3 @@ -112,6 +112,13 @@
1.4
1.5 *** HOL ***
1.6
1.7 +* Abstract algebra:
1.8 + * class division_by_zero includes division_ring;
1.9 + * numerous lemmas have been ported from field to division_ring;
1.10 + * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
1.11 +
1.12 + INCOMPATIBILITY.
1.13 +
1.14 * Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
1.15 provides abstract red-black tree type which is backed by RBT_Impl
1.16 as implementation. INCOMPATIBILTY.