NEWS
changeset 8655 16906e600c9a
parent 8626 76e3913ff421
child 8673 987ea1a559d0
     1.1 --- a/NEWS	Sat Apr 01 20:16:56 2000 +0200
     1.2 +++ b/NEWS	Sat Apr 01 20:17:51 2000 +0200
     1.3 @@ -12,8 +12,8 @@
     1.4  
     1.5  * HOL: simplification no longer dives into case-expressions
     1.6  
     1.7 -* HOL: the recursion equations generated by `recdef' are now called
     1.8 -  f.simps instead of f.rules.
     1.9 +* HOL: the recursion equations generated by 'recdef' are now called
    1.10 +f.simps instead of f.rules;
    1.11  
    1.12  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.13  
    1.14 @@ -106,12 +106,11 @@
    1.15  t.weak_case_cong from the simpset, either permanently
    1.16  (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
    1.17  
    1.18 -* the recursion equations generated by `recdef' for function `f' are now
    1.19 -called f.simps instead of f.rules. If all termination conditions are proved
    1.20 -automatically, these simplification rules are added to the simpset, as in
    1.21 -primrec. These simplification rules are numbered canonically: all equations
    1.22 -generated from clauses i are called "f.i"; counting starts with 0. These
    1.23 -equations can be removed from the simpset like this: delsimps (thms"f.i").
    1.24 +* the recursion equations generated by 'recdef' for function 'f' are
    1.25 +now called f.simps instead of f.rules; if all termination conditions
    1.26 +are proved automatically, these simplification rules are added to the
    1.27 +simpset, as in primrec; rules may be named individually as well,
    1.28 +resulting in a separate list of theorems for each equation;
    1.29  
    1.30  
    1.31  *** General ***