| changeset 13613 | 531f1f524848 |
| parent 13587 | 659813a3f879 |
| child 13618 | 12290bdce807 |
--- a/NEWS Mon Sep 30 16:48:15 2002 +0200 +++ b/NEWS Mon Sep 30 16:50:39 2002 +0200 @@ -74,6 +74,9 @@ * the simplifier trace now shows the names of the applied rewrite rules +* induct over a !!-quantified statement (say !!x1..xn): + each "case" automatically performs "fix x1 .. xn" with exactly those names. + * GroupTheory: converted to Isar theories, using locales with implicit structures; * Real/HahnBanach: updated and adapted to locales;