author | wenzelm |

Thu Aug 29 16:15:11 2002 +0200 (2002-08-29) | |

changeset 13549 | f1522b892a4c |

parent 13548 | 36cb5fb8188c |

child 13550 | 5a176b8dda84 |

updated;

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