# HG changeset patch
# User ballarin
# Date 1052493598 -7200
# Node ID ab988a7a8a3b9416b5aa3092f844cb7161b1b429
# Parent  aa78df2e254b33cf2d71cf7a51a031d066216309
NEWS updated for HOL-Algebra.

diff -r aa78df2e254b -r ab988a7a8a3b 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;