--- a/NEWS Mon Aug 18 19:18:08 2014 +0200
+++ b/NEWS Tue Aug 19 09:34:27 2014 +0200
@@ -33,6 +33,13 @@
strong_coinduct ~> coinduct_strong
weak_case_cong ~> case_cong_weak
INCOMPATIBILITY.
+ - The rule "set_cases" is registered with the "[cases set]"
+ attribute. This can influence the behavior of the "cases" proof
+ method when more than one case rule is applicable (e.g., an
+ assumption is of the form "w : set ws" and the method "cases w"
+ is invoked). The solution is to specify the case rule explicitly
+ (e.g. "cases w rule: widget.exhaust").
+ INCOMPATIBILITY.
* Old datatype package:
- Renamed theorems: