# HG changeset patch
# User paulson
# Date 1048176916 -3600
# Node ID 601514e635340ad6196823723e0e009c502aadd6
# Parent  26e5f5e624f6eb0231ee89a4dd4d5ce72de4dd89
Gauss, UNITY, ZF

diff -r 26e5f5e624f6 -r 601514e63534 NEWS
--- a/NEWS	Thu Mar 20 15:58:25 2003 +0100
+++ b/NEWS	Thu Mar 20 17:15:16 2003 +0100
@@ -103,8 +103,6 @@
 
 *** HOL ***
 
-* GroupTheory: new, experimental summation operator for abelian groups.
-
 * New tactic "trans_tac" and method "trans" instantiate
 Provers/linorder.ML for axclasses "order" and "linorder" (predicates
 "<=", "<" and "="). 
@@ -142,17 +140,23 @@
 * induct over a !!-quantified statement (say !!x1..xn):
   each "case" automatically performs "fix x1 .. xn" with exactly those names.
 
-* GroupTheory: converted to Isar theories, using locales with implicit structures;
-
 * 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);
+
+* UNITY: added the Meier-Sanders theory of progress sets;
+
 
 *** ZF ***
 
 * ZF/Constructible: consistency proof for AC (Gödel's constructible
 universe, etc.);
 
-* Main ZF: many theories converted to new-style format;
+* Main ZF: virtually all theories converted to new-style format;
 
 
 *** ML ***