author | paulson |

Mon May 05 18:34:16 2003 +0200 (2003-05-05) | |

changeset 13960 | 70f9158b6695 |

parent 13959 | 0e0553e7d696 |

child 13961 | 233dd3bb2390 |

Complex, etc

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