# HG changeset patch
# User blanchet
# Date 1408433667 -7200
# Node ID 90d941a477bd82f4849006fb59ec7d703d4d54c4
# Parent  45873fcbbf2ebd7636d9567b1a352aa9d0e2ebe3
documented slight incompatibility in NEWS

diff -r 45873fcbbf2e -r 90d941a477bd NEWS
--- 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: