summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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