--- a/NEWS Fri Oct 19 10:46:42 2012 +0200
+++ b/NEWS Fri Oct 19 15:12:52 2012 +0200
@@ -76,7 +76,6 @@
written just "typedef t = A". INCOMPATIBILITY, need to adapt theories
accordingly.
-
* Theory "Library/Multiset":
- Renamed constants
@@ -142,6 +141,13 @@
INCOMPATIBILITY.
+* HOL/Rings: renamed lemmas
+
+left_distrib ~> distrib_right
+right_distrib ~> distrib_left
+
+in class semiring. INCOMPATIBILITY.
+
* HOL/BNF: New (co)datatype package based on bounded natural
functors with support for mixed, nested recursion and interesting
non-free datatypes.