Updates to HOL/Algebra:
- axclasses consolidated (lemma one_not_zero)
- summation operator SUM removed, now uses setsum
Use of setsum made it necessary to relax sort constraint in its definition
to {zero, plus}.

--- a/NEWS	Fri Feb 09 23:48:50 2001 +0100
+++ b/NEWS	Sat Feb 10 08:48:10 2001 +0100
@@ -7,6 +7,12 @@
 
 *** Overview of INCOMPATIBILITIES ***
 
+* HOL/Algebra: special summation operator SUM no longer exists, it has
+been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd');
+
+* HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring'
+to 'domain', this makes the theory consistent with mathematical literature;
+ 
 * HOL: inductive package no longer splits induction rule aggressively,
 but only as far as specified by the introductions given; the old
 format may recovered via ML function complete_split_rule or attribute