# HG changeset patch
# User nipkow
# Date 954332607 -7200
# Node ID 805910de7be0a08f069f08e25e3dfb16d890c7e9
# Parent  f077613e8e7bfc231f45efb194b40820be5e8893
*** empty log message ***

diff -r f077613e8e7b -r 805910de7be0 NEWS
--- a/NEWS	Tue Mar 28 17:33:44 2000 +0200
+++ b/NEWS	Wed Mar 29 14:23:27 2000 +0200
@@ -11,6 +11,8 @@
 
 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
 
+* HOL: simplification no longer dives into case-expressions
+
 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
 
 
@@ -89,6 +91,12 @@
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
 exists, may define val exhaust_tac = case_tac for ad-hoc portability;
 
+* HOL: simplification no longer dives into case-expressions: only the
+selector expression is simplified, but not the remaining arms. To enable full
+simplification of case-expressions for datatype t, you need to remove
+t.weak_case_cong from the simpset, either permanently
+(Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
+
 
 *** General ***