NEWS
changeset 13549 f1522b892a4c
parent 13541 44efea0e21fa
child 13550 5a176b8dda84
     1.1 --- a/NEWS	Thu Aug 29 16:08:32 2002 +0200
     1.2 +++ b/NEWS	Thu Aug 29 16:15:11 2002 +0200
     1.3 @@ -63,8 +63,18 @@
     1.4  * simp's arithmetic capabilities have been enhanced a bit: it now
     1.5  takes ~= in premises into account (by performing a case split);
     1.6  
     1.7 -* simp reduces "m*(n div m) + n mod m" to n, even if the two summands are
     1.8 -  distributed over a sum of terms.
     1.9 +* simp reduces "m*(n div m) + n mod m" to n, even if the two summands
    1.10 +are distributed over a sum of terms;
    1.11 +
    1.12 +* Real/HahnBanach: updated and adapted to locales;
    1.13 +
    1.14 +
    1.15 +*** ZF ***
    1.16 +
    1.17 +* ZF/Constructible: consistency proof for AC (Gödel's constructible
    1.18 +universe, etc.);
    1.19 +
    1.20 +* Main ZF: many theories converted to new-style format;
    1.21  
    1.22  
    1.23  *** ML ***