--- 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 ***