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