diff -r 36cb5fb8188c -r f1522b892a4c NEWS
--- 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 ***