# HG changeset patch
# User krauss
# Date 1162888874 -3600
# Node ID 2f6e276bfb930d4aa12febcb9b09f8ec4a21288c
# Parent  2d83f93c358088de481457468fab62430ccec09a
updated NEWS

diff -r 2d83f93c3580 -r 2f6e276bfb93 NEWS
--- a/NEWS	Tue Nov 07 09:33:47 2006 +0100
+++ b/NEWS	Tue Nov 07 09:41:14 2006 +0100
@@ -475,6 +475,18 @@
 
 *** HOL ***
 
+* axclass "semiring_0" now contains annihilation axioms 
+("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer 
+structures do not inherit from semiring_0 anymore, because this property 
+is a theorem there, not an axiom.
+INCOMPATIBILITY: In instances of semiring_0, there is more to prove, but 
+this is mostly trivial.
+
+* axclass "recpower" was generalized to arbitrary monoids, not just 
+commutative semirings.
+INCOMPATIBILITY: If you use recpower and need commutativity or a semiring
+property, add the corresponding classes.
+
 * Constant "List.list_all2" in List.thy now uses authentic syntax.
 INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar
 level, use abbreviations instead.