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