diff -r c03318d3f37c -r 3ef6c509f29c NEWS
--- a/NEWS Mon May 12 15:49:37 2003 +0200
+++ b/NEWS Mon May 12 15:51:34 2003 +0200
@@ -152,9 +152,10 @@
%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 formalization of ring theory and
-and univariate polynomials;
+* Algebra: formalization of classical algebra. Intended as base for
+any algebraic development in Isabelle. Currently covers group theory
+(up to Sylow's theorem) and ring theory (Universal Property of
+Univariate Polynomials). Contributions welcome;
* GroupTheory: deleted, since its material has been moved to Algebra;