# HG changeset patch
# User nipkow
# Date 954439587 -7200
# Node ID 76e3913ff421cc493a061043d1c180fb2d4f2871
# Parent  93a11ebacf32aa5915635156a93de7efe9cba413
recdef

diff -r 93a11ebacf32 -r 76e3913ff421 NEWS
--- 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 ***