*** empty log message ***
authornipkow
Wed Mar 29 14:23:27 2000 +0200 (2000-03-29)
changeset 8603805910de7be0
parent 8602 f077613e8e7b
child 8604 c99e0024050c
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Tue Mar 28 17:33:44 2000 +0200
     1.2 +++ b/NEWS	Wed Mar 29 14:23:27 2000 +0200
     1.3 @@ -11,6 +11,8 @@
     1.4  
     1.5  * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
     1.6  
     1.7 +* HOL: simplification no longer dives into case-expressions
     1.8 +
     1.9  * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
    1.10  
    1.11  
    1.12 @@ -89,6 +91,12 @@
    1.13  "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
    1.14  exists, may define val exhaust_tac = case_tac for ad-hoc portability;
    1.15  
    1.16 +* HOL: simplification no longer dives into case-expressions: only the
    1.17 +selector expression is simplified, but not the remaining arms. To enable full
    1.18 +simplification of case-expressions for datatype t, you need to remove
    1.19 +t.weak_case_cong from the simpset, either permanently
    1.20 +(Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]).
    1.21 +
    1.22  
    1.23  *** General ***
    1.24