NEWS
changeset 36298 c805033ad032
parent 36201 07d4f74abd12
child 36317 506d732cb522
     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.