--- a/NEWS Thu Aug 29 16:08:32 2002 +0200
+++ b/NEWS Thu Aug 29 16:15:11 2002 +0200
@@ -63,8 +63,18 @@
* simp's arithmetic capabilities have been enhanced a bit: it now
takes ~= in premises into account (by performing a case split);
-* simp reduces "m*(n div m) + n mod m" to n, even if the two summands are
- distributed over a sum of terms.
+* simp reduces "m*(n div m) + n mod m" to n, even if the two summands
+are distributed over a sum of terms;
+
+* Real/HahnBanach: updated and adapted to locales;
+
+
+*** ZF ***
+
+* ZF/Constructible: consistency proof for AC (Gödel's constructible
+universe, etc.);
+
+* Main ZF: many theories converted to new-style format;
*** ML ***