equal
deleted
inserted
replaced
1 |
|
2 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
3 ============================================== |
2 ============================================== |
4 |
3 |
5 New in this Isabelle release |
4 New in this Isabelle release |
6 ---------------------------- |
5 ---------------------------- |
67 * simp's arithmetic capabilities have been enhanced a bit: it now |
66 * simp's arithmetic capabilities have been enhanced a bit: it now |
68 takes ~= in premises into account (by performing a case split); |
67 takes ~= in premises into account (by performing a case split); |
69 |
68 |
70 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands |
69 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands |
71 are distributed over a sum of terms; |
70 are distributed over a sum of terms; |
|
71 |
|
72 * the simplifier trace now shows the names of the applied rewrite rules |
72 |
73 |
73 * Real/HahnBanach: updated and adapted to locales; |
74 * Real/HahnBanach: updated and adapted to locales; |
74 |
75 |
75 |
76 |
76 *** ZF *** |
77 *** ZF *** |