--- a/NEWS Mon Oct 15 21:04:32 2001 +0200
+++ b/NEWS Mon Oct 15 21:04:46 2001 +0200
@@ -40,6 +40,8 @@
* HOL: 'inductive' now longer features separate (collective)
attributes for 'intros';
+* HOL: canonical 'cases'/'induct' rules for n-tuples (n=3..7)
+
*** HOL ***