# HG changeset patch
# User ballarin
# Date 1052747494 -7200
# Node ID 3ef6c509f29c6c8e76cd0c86dab43877d6c640b0
# Parent  c03318d3f37ccfa6acb0376f8b994ef776043e44
Improved entry on Algebra.

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;