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

author | ballarin |

Fri, 09 May 2003 17:19:58 +0200 | |

changeset 13995 | ab988a7a8a3b |

parent 13994 | aa78df2e254b |

child 13996 | a994b92ab1ea |

NEWS updated for HOL-Algebra.

--- 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;