# HG changeset patch
# User wenzelm
# Date 954613071 -7200
# Node ID 16906e600c9afd09bae796f0d9b8c001e19c11a2
# Parent  38ce936acb994bbffdb8e32ca1802c93f545d259
recdef: admit name and atts;

diff -r 38ce936acb99 -r 16906e600c9a NEWS
--- 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 ***