# HG changeset patch
# User wenzelm
# Date 970492354 -7200
# Node ID a62b275ac0f7c892a67740bb670ce65498dafa8a
# Parent  98ddd0138cbf98b7a0d76746b3378ac1a445bfed
improved t.weak_case_cong text;

diff -r 98ddd0138cbf -r a62b275ac0f7 NEWS
--- a/NEWS	Mon Oct 02 14:59:04 2000 +0200
+++ b/NEWS	Mon Oct 02 15:12:34 2000 +0200
@@ -14,7 +14,8 @@
   Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 
-* HOL: simplification no longer dives into case-expressions;
+* HOL: simplification no longer dives into case-expressions; this is
+controlled by "t.weak_case_cong" for each datatype t;
 
 * HOL: nat_less_induct renamed to less_induct;
 
@@ -275,10 +276,10 @@
 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 [...]).
+selector expression is simplified, but not the remaining arms; to
+enable full simplification of case-expressions for datatype t, you may
+remove t.weak_case_cong from the simpset, either globally (Delcongs
+[thm"t.weak_case_cong"];) or locally (delcongs [...]).
 
 * HOL/recdef: the recursion equations generated by 'recdef' for
 function 'f' are now called f.simps instead of f.rules; if all