# HG changeset patch
# User kleing
# Date 1003172686 -7200
# Node ID 60054fee3c16b9f692add2730eacd38d3c3e9612
# Parent  85b3735a51e17af3e97072ede06de9138bbdb64b
canonical 'cases'/'induct' rules for n-tuples (n=3..7)

diff -r 85b3735a51e1 -r 60054fee3c16 NEWS
--- 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 ***