NEWS
changeset 59868 b1cd0c962780
parent 59849 c3d126c7944f
child 59870 68d6b6aa4450
     1.1 --- a/NEWS	Tue Mar 31 21:54:32 2015 +0200
     1.2 +++ b/NEWS	Tue Mar 31 21:54:32 2015 +0200
     1.3 @@ -89,6 +89,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Given up separate type class no_zero_divisors in favour of fully algebraic
     1.8 +semiring_no_zero_divisors.  INCOMPATIBILITY.
     1.9 +
    1.10 +* Class linordered_semidom really requires no zero divisors.
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13 +* Classes division_ring, field and linordered_field always demand
    1.14 +`inverse 0 = 0`.  Given up separate classes division_ring_inverse_zero,
    1.15 +field_inverse_zero and linordered_field_inverse_zero.
    1.16 +INCOMPATIBILITY.
    1.17 +
    1.18  * Type classes cancel_ab_semigroup_add / cancel_monoid_add specify
    1.19  explicit additive inverse operation.  INCOMPATIBILITY.
    1.20