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

NEWS

changeset 13995 | ab988a7a8a3b |

parent 13966 | 2160abf7cfe7 |

child 14008 | f843528b9f3c |

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