equal
deleted
inserted
replaced
71 |
71 |
72 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands |
72 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands |
73 are distributed over a sum of terms; |
73 are distributed over a sum of terms; |
74 |
74 |
75 * the simplifier trace now shows the names of the applied rewrite rules |
75 * the simplifier trace now shows the names of the applied rewrite rules |
|
76 |
|
77 * induct over a !!-quantified statement (say !!x1..xn): |
|
78 each "case" automatically performs "fix x1 .. xn" with exactly those names. |
76 |
79 |
77 * GroupTheory: converted to Isar theories, using locales with implicit structures; |
80 * GroupTheory: converted to Isar theories, using locales with implicit structures; |
78 |
81 |
79 * Real/HahnBanach: updated and adapted to locales; |
82 * Real/HahnBanach: updated and adapted to locales; |
80 |
83 |