Updates to HOL/Algebra:
authorballarin
Sat Feb 10 08:48:10 2001 +0100 (2001-02-10)
changeset 1109145ffef3d3e75
parent 11090 3041d0347d26
child 11092 69c1abb9a129
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}.
NEWS
     1.1 --- a/NEWS	Fri Feb 09 23:48:50 2001 +0100
     1.2 +++ b/NEWS	Sat Feb 10 08:48:10 2001 +0100
     1.3 @@ -7,6 +7,12 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 +* HOL/Algebra: special summation operator SUM no longer exists, it has
     1.8 +been replaced by setsum; infix 'assoc' now has priority 50 (like 'dvd');
     1.9 +
    1.10 +* HOL/Algebra: axiom 'one_not_zero' has been moved from axclass 'ring'
    1.11 +to 'domain', this makes the theory consistent with mathematical literature;
    1.12 + 
    1.13  * HOL: inductive package no longer splits induction rule aggressively,
    1.14  but only as far as specified by the introductions given; the old
    1.15  format may recovered via ML function complete_split_rule or attribute