# HG changeset patch
# User ballarin
# Date 981791290 -3600
# Node ID 45ffef3d3e752dab4e4cffce29b50c78071a2221
# Parent  3041d0347d26b8792e174cf60f8750dfe3bdb02b
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}.

diff -r 3041d0347d26 -r 45ffef3d3e75 NEWS
--- 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