NEWS

changeset 13995 | ab988a7a8a3b |

parent 13966 | 2160abf7cfe7 |

child 14008 | f843528b9f3c |

--- a/NEWS Fri May 09 14:21:07 2003 +0200 +++ b/NEWS Fri May 09 17:19:58 2003 +0200 @@ -148,9 +148,9 @@ %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; +* Algebra: contains a new formalization of group theory, using locales +with implicit structures. Also a new formalization of ring theory and +and univariate polynomials; * GroupTheory: deleted, since its material has been moved to Algebra; @@ -165,8 +165,8 @@ * Real/HahnBanach: updated and adapted to locales; -* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, Gray and -Kramer); +* NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad, +Gray and Kramer); * UNITY: added the Meier-Sanders theory of progress sets;