--- a/NEWS Sat Apr 01 20:16:56 2000 +0200
+++ b/NEWS Sat Apr 01 20:17:51 2000 +0200
@@ -12,8 +12,8 @@
* HOL: simplification no longer dives into case-expressions
-* HOL: the recursion equations generated by `recdef' are now called
- f.simps instead of f.rules.
+* 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;
@@ -106,12 +106,11 @@
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").
+* 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; rules may be named individually as well,
+resulting in a separate list of theorems for each equation;
*** General ***