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

author | wenzelm |

Mon, 02 Oct 2000 15:12:34 +0200 | |

changeset 10129 | a62b275ac0f7 |

parent 10128 | 98ddd0138cbf |

child 10130 | 5a2e00bf1e42 |

improved t.weak_case_cong text;

--- a/NEWS Mon Oct 02 14:59:04 2000 +0200 +++ b/NEWS Mon Oct 02 15:12:34 2000 +0200 @@ -14,7 +14,8 @@ Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; -* HOL: simplification no longer dives into case-expressions; +* HOL: simplification no longer dives into case-expressions; this is +controlled by "t.weak_case_cong" for each datatype t; * HOL: nat_less_induct renamed to less_induct; @@ -275,10 +276,10 @@ 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 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 [...]). +selector expression is simplified, but not the remaining arms; to +enable full simplification of case-expressions for datatype t, you may +remove t.weak_case_cong from the simpset, either globally (Delcongs +[thm"t.weak_case_cong"];) or locally (delcongs [...]). * HOL/recdef: the recursion equations generated by 'recdef' for function 'f' are now called f.simps instead of f.rules; if all