NEWS
changeset 49962 a8cc904a6820
parent 49918 cf441f4a358b
child 49963 326f87427719
     1.1 --- a/NEWS	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/NEWS	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -76,7 +76,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 @@ -142,6 +141,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.