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

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