# HG changeset patch
# User paulson
# Date 1052152456 -7200
# Node ID 70f9158b66957e06c72ecc3d774ca1b37ba0a3ca
# Parent  0e0553e7d6961a52a4429808b9094be171c9450f
Complex, etc

diff -r 0e0553e7d696 -r 70f9158b6695 NEWS
--- a/NEWS	Mon May 05 18:30:48 2003 +0200
+++ b/NEWS	Mon May 05 18:34:16 2003 +0200
@@ -148,11 +148,18 @@
 %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;
+
+* Complex: new directory of the complex numbers with numeric constants, nonstandard complex numbers, and some complex analysis, standard and nonstandard (Jacques Fleuriot);
+
+* GroupTheory: deleted, since its material has been moved to Algebra;
+
+* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques Fleuriot);
+
 * Real/HahnBanach: updated and adapted to locales;
 
-* GroupTheory: converted to Isar theories, using locales with implicit
-structures.  Also a new, experimental summation operator for abelian groups;
-
 * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and
 Kramer);