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

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