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

author | wenzelm |

Sat, 01 Apr 2000 20:17:51 +0200 | |

changeset 8655 | 16906e600c9a |

parent 8654 | 38ce936acb99 |

child 8656 | 1062572b5b37 |

recdef: admit name and atts;

--- 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 ***