--- a/NEWS Thu Mar 30 19:47:17 2000 +0200
+++ b/NEWS Thu Mar 30 20:06:27 2000 +0200
@@ -1,4 +1,3 @@
-
Isabelle NEWS -- history user-relevant changes
==============================================
@@ -13,6 +12,9 @@
* HOL: simplification no longer dives into case-expressions
+* HOL: the recursion equations generated by `recdef' are now called
+ f.simps instead of f.rules.
+
* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
@@ -98,12 +100,19 @@
"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 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 [...]).
+* the recursion equations generated by `recdef' for function `f' are now
+called f.simps instead of f.rules. If all termination conditions are proved
+automatically, these simplification rules are added to the simpset, as in
+primrec. These simplification rules are numbered canonically: all equations
+generated from clauses i are called "f.i"; counting starts with 0. These
+equations can be removed from the simpset like this: delsimps (thms"f.i").
+
*** General ***