Complex, etc
authorpaulson
Mon, 05 May 2003 18:34:16 +0200
changeset 13960 70f9158b6695
parent 13959 0e0553e7d696
child 13961 233dd3bb2390
Complex, etc
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);