1.1 --- a/NEWS	Sun Oct 21 16:43:08 2012 +0200
     1.2 +++ b/NEWS	Sun Oct 21 17:04:13 2012 +0200
     1.3 @@ -79,7 +79,6 @@
     1.4  written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
     1.5  accordingly.
     1.6  
     1.7 -
     1.8  * Theory "Library/Multiset":
     1.9  
    1.10    - Renamed constants
    1.11 @@ -145,6 +144,13 @@
    1.12  
    1.13      INCOMPATIBILITY.
    1.14  
    1.15 +* HOL/Rings: renamed lemmas
    1.16 +
    1.17 +left_distrib ~> distrib_right
    1.18 +right_distrib ~> distrib_left
    1.19 +
    1.20 +in class semiring.  INCOMPATIBILITY.
    1.21 +
    1.22  * HOL/BNF: New (co)datatype package based on bounded natural
    1.23  functors with support for mixed, nested recursion and interesting
    1.24  non-free datatypes.