# HG changeset patch
# User wenzelm
# Date 1213176010 -7200
# Node ID 0337828b7815d6973e15b2b83b07567949ee619a
# Parent  ef2634bef947b0a1074587647247fdd32c3c227d
tuned;

diff -r ef2634bef947 -r 0337828b7815 NEWS
--- a/NEWS	Wed Jun 11 09:08:52 2008 +0200
+++ b/NEWS	Wed Jun 11 11:20:10 2008 +0200
@@ -19,7 +19,8 @@
 the corresponding "cases" and "induct" attributes.  INCOMPATIBILITY,
 in rare situations a different rule is selected --- notably nested
 tuple elimination instead of former prod.exhaust: use explicit
-(case_tac t rule: prod.exhaust) here.
+(case_tac t rule: prod.exhaust) here.  Old-style rules for mutual and
+nested datatypes also need to be given explicitly.
 
 * Attributes "cases", "induct", "coinduct" support "del" option.