NEWS updated for HOL-Algebra.
authorballarin
Fri, 09 May 2003 17:19:58 +0200
changeset 13995 ab988a7a8a3b
parent 13994 aa78df2e254b
child 13996 a994b92ab1ea
NEWS updated for HOL-Algebra.
NEWS
--- a/NEWS	Fri May 09 14:21:07 2003 +0200
+++ b/NEWS	Fri May 09 17:19:58 2003 +0200
@@ -148,9 +148,9 @@
 %x. None. Warning: empty_def now refers to the previously hidden definition
 of the empty set.
 
-* Algebra: contains a new formalization of group theory, using locales with
-implicit structures.  Also a new, experimental summation operator for
-abelian groups;
+* Algebra: contains a new formalization of group theory, using locales
+with implicit structures.  Also a new formalization of ring theory and
+and univariate polynomials;
 
 * GroupTheory: deleted, since its material has been moved to Algebra;
 
@@ -165,8 +165,8 @@
 
 * Real/HahnBanach: updated and adapted to locales;
 
-* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and
-Kramer);
+* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad,
+Gray and Kramer);
 
 * UNITY: added the Meier-Sanders theory of progress sets;