summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 13549 | f1522b892a4c |

parent 13541 | 44efea0e21fa |

child 13550 | 5a176b8dda84 |

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