NEWS updated for HOL-Algebra.
--- 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;