summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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