NEWS
changeset 13960 70f9158b6695
parent 13954 2e989faba65a
child 13966 2160abf7cfe7
     1.1 --- a/NEWS	Mon May 05 18:30:48 2003 +0200
     1.2 +++ b/NEWS	Mon May 05 18:34:16 2003 +0200
     1.3 @@ -148,11 +148,18 @@
     1.4  %x. None. Warning: empty_def now refers to the previously hidden definition
     1.5  of the empty set.
     1.6  
     1.7 +* Algebra: contains a new formalization of group theory, using locales with
     1.8 +implicit structures.  Also a new, experimental summation operator for
     1.9 +abelian groups;
    1.10 +
    1.11 +* Complex: new directory of the complex numbers with numeric constants, nonstandard complex numbers, and some complex analysis, standard and nonstandard (Jacques Fleuriot);
    1.12 +
    1.13 +* GroupTheory: deleted, since its material has been moved to Algebra;
    1.14 +
    1.15 +* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques Fleuriot);
    1.16 +
    1.17  * Real/HahnBanach: updated and adapted to locales;
    1.18  
    1.19 -* GroupTheory: converted to Isar theories, using locales with implicit
    1.20 -structures.  Also a new, experimental summation operator for abelian groups;
    1.21 -
    1.22  * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and
    1.23  Kramer);
    1.24