NEWS
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;