NEWS
changeset 8626 76e3913ff421
parent 8621 8ba0f90f6f35
child 8655 16906e600c9a
     1.1 --- a/NEWS	Thu Mar 30 19:47:17 2000 +0200
     1.2 +++ b/NEWS	Thu Mar 30 20:06:27 2000 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -13,6 +12,9 @@
     1.9  
    1.10  * HOL: simplification no longer dives into case-expressions
    1.11  
    1.12 +* HOL: the recursion equations generated by `recdef' are now called
    1.13 +  f.simps instead of f.rules.
    1.14 +
    1.15  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.16  
    1.17  
    1.18 @@ -98,12 +100,19 @@
    1.19  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
    1.20  exists, may define val exhaust_tac = case_tac for ad-hoc portability;
    1.21  
    1.22 -* HOL: simplification no longer dives into case-expressions: only the
    1.23 -selector expression is simplified, but not the remaining arms. To enable full
    1.24 +* simplification no longer dives into case-expressions: only the selector
    1.25 +expression is simplified, but not the remaining arms. To enable full
    1.26  simplification of case-expressions for datatype t, you need to remove
    1.27  t.weak_case_cong from the simpset, either permanently
    1.28  (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
    1.29  
    1.30 +* the recursion equations generated by `recdef' for function `f' are now
    1.31 +called f.simps instead of f.rules. If all termination conditions are proved
    1.32 +automatically, these simplification rules are added to the simpset, as in
    1.33 +primrec. These simplification rules are numbered canonically: all equations
    1.34 +generated from clauses i are called "f.i"; counting starts with 0. These
    1.35 +equations can be removed from the simpset like this: delsimps (thms"f.i").
    1.36 +
    1.37  
    1.38  *** General ***
    1.39