# HG changeset patch
# User noschinl
# Date 1318854134 -7200
# Node ID b09575e075a52ef4d489c47c8e2501e3f321ab89
# Parent  3f1d1ce024cb17072501209173993f53ef2b06ae
(old) NEWS

diff -r 3f1d1ce024cb -r b09575e075a5 NEWS
--- a/NEWS	Mon Oct 17 10:19:01 2011 +0200
+++ b/NEWS	Mon Oct 17 14:22:14 2011 +0200
@@ -53,6 +53,18 @@
   zero_less_zpower_abs_iff ~> zero_less_power_abs_iff
   zero_le_zpower_abs ~> zero_le_power_abs
 
+* New case_product attribute to generate a case rule doing multiple case
+  distinctions at the same time: E.g.
+
+    list.exhaust[case_product nat.exhaust]
+
+  produces a rule which can be used to perform case distinction on both
+  a list and a nat.
+
+*** FOL ***
+
+* New case_product attribute (see HOL).
+
 
 *** ML ***