NEWS
changeset 13966 2160abf7cfe7
parent 13960 70f9158b6695
child 13995 ab988a7a8a3b
     1.1 --- a/NEWS	Tue May 06 12:29:49 2003 +0200
     1.2 +++ b/NEWS	Tue May 06 17:45:54 2003 +0200
     1.3 @@ -152,11 +152,16 @@
     1.4  implicit structures.  Also a new, experimental summation operator for
     1.5  abelian groups;
     1.6  
     1.7 -* Complex: new directory of the complex numbers with numeric constants, nonstandard complex numbers, and some complex analysis, standard and nonstandard (Jacques Fleuriot);
     1.8 -
     1.9  * GroupTheory: deleted, since its material has been moved to Algebra;
    1.10  
    1.11 -* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques Fleuriot);
    1.12 +* Complex: new directory of the complex numbers with numeric constants, 
    1.13 +nonstandard complex numbers, and some complex analysis, standard and 
    1.14 +nonstandard (Jacques Fleuriot);
    1.15 +
    1.16 +* HOL-Complex: new image for analysis, replacing HOL-Real and HOL-Hyperreal;
    1.17 +
    1.18 +* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques 
    1.19 +Fleuriot);
    1.20  
    1.21  * Real/HahnBanach: updated and adapted to locales;
    1.22