summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 05 May 2003 18:34:16 +0200 | |

changeset 13960 | 70f9158b6695 |

parent 13959 | 0e0553e7d696 |

child 13961 | 233dd3bb2390 |

Complex, etc

--- a/NEWS Mon May 05 18:30:48 2003 +0200 +++ b/NEWS Mon May 05 18:34:16 2003 +0200 @@ -148,11 +148,18 @@ %x. None. Warning: empty_def now refers to the previously hidden definition of the empty set. +* Algebra: contains a new formalization of group theory, using locales with +implicit structures. Also a new, experimental summation operator for +abelian groups; + +* Complex: new directory of the complex numbers with numeric constants, nonstandard complex numbers, and some complex analysis, standard and nonstandard (Jacques Fleuriot); + +* GroupTheory: deleted, since its material has been moved to Algebra; + +* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques Fleuriot); + * Real/HahnBanach: updated and adapted to locales; -* GroupTheory: converted to Isar theories, using locales with implicit -structures. Also a new, experimental summation operator for abelian groups; - * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and Kramer);