NEWS
changeset 8626 76e3913ff421
parent 8621 8ba0f90f6f35
child 8655 16906e600c9a
--- 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 ***