NEWS
changeset 13995 ab988a7a8a3b
parent 13966 2160abf7cfe7
child 14008 f843528b9f3c
     1.1 --- a/NEWS	Fri May 09 14:21:07 2003 +0200
     1.2 +++ b/NEWS	Fri May 09 17:19:58 2003 +0200
     1.3 @@ -148,9 +148,9 @@
     1.4  %x. None. Warning: empty_def now refers to the previously hidden definition
     1.5  of the empty set.
     1.6  
     1.7 -* Algebra: contains a new formalization of group theory, using locales with
     1.8 -implicit structures.  Also a new, experimental summation operator for
     1.9 -abelian groups;
    1.10 +* Algebra: contains a new formalization of group theory, using locales
    1.11 +with implicit structures.  Also a new formalization of ring theory and
    1.12 +and univariate polynomials;
    1.13  
    1.14  * GroupTheory: deleted, since its material has been moved to Algebra;
    1.15  
    1.16 @@ -165,8 +165,8 @@
    1.17  
    1.18  * Real/HahnBanach: updated and adapted to locales;
    1.19  
    1.20 -* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and
    1.21 -Kramer);
    1.22 +* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad,
    1.23 +Gray and Kramer);
    1.24  
    1.25  * UNITY: added the Meier-Sanders theory of progress sets;
    1.26