Improved entry on Algebra.
authorballarin
Mon, 12 May 2003 15:51:34 +0200
changeset 14018 3ef6c509f29c
parent 14017 c03318d3f37c
child 14019 b141b26145e1
Improved entry on Algebra.
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;