1.1 --- a/NEWS	Mon Sep 30 16:48:15 2002 +0200
     1.2 +++ b/NEWS	Mon Sep 30 16:50:39 2002 +0200
     1.3 @@ -74,6 +74,9 @@
     1.4  
     1.5  * the simplifier trace now shows the names of the applied rewrite rules
     1.6  
     1.7 +* induct over a !!-quantified statement (say !!x1..xn):
     1.8 +  each "case" automatically performs "fix x1 .. xn" with exactly those names.
     1.9 +
    1.10  * GroupTheory: converted to Isar theories, using locales with implicit structures;
    1.11  
    1.12  * Real/HahnBanach: updated and adapted to locales;