summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 30 Mar 2000 20:06:27 +0200 | |

changeset 8626 | 76e3913ff421 |

parent 8625 | 93a11ebacf32 |

child 8627 | 44ec33bb5c5b |

recdef

--- a/NEWS Thu Mar 30 19:47:17 2000 +0200 +++ b/NEWS Thu Mar 30 20:06:27 2000 +0200 @@ -1,4 +1,3 @@ - Isabelle NEWS -- history user-relevant changes ============================================== @@ -13,6 +12,9 @@ * HOL: simplification no longer dives into case-expressions +* 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; @@ -98,12 +100,19 @@ "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer exists, may define val exhaust_tac = case_tac for ad-hoc portability; -* HOL: simplification no longer dives into case-expressions: only the -selector expression is simplified, but not the remaining arms. To enable full +* simplification no longer dives into case-expressions: only the selector +expression is simplified, but not the remaining arms. To enable full simplification of case-expressions for datatype t, you need to remove 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"). + *** General ***