# HG changeset patch
# User traytel
# Date 1365608956 -7200
# Node ID bdaa1582dc8b3daf6667ea9f5d00e53785206a7e
# Parent  bdfa3b947992a894e5dde70e6778d23e0c5aaf37
NEWS and CONTRIBUTORS

diff -r bdfa3b947992 -r bdaa1582dc8b CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Apr 10 17:49:16 2013 +0200
+++ b/CONTRIBUTORS	Wed Apr 10 17:49:16 2013 +0200
@@ -6,6 +6,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* April 2013: Stefan Berghofer, secunet Security Networks AG
+  Dmitriy Traytel, TUM
+  Makarius Wenzel, Université Paris-Sud / LRI
+  Case translations as a separate check phase independent of the
+  datatype package.
+
 * March 2013: Florian Haftmann, TUM
   Reform of "big operators" on sets.
 
diff -r bdfa3b947992 -r bdaa1582dc8b NEWS
--- a/NEWS	Wed Apr 10 17:49:16 2013 +0200
+++ b/NEWS	Wed Apr 10 17:49:16 2013 +0200
@@ -43,6 +43,13 @@
 
 *** HOL ***
 
+* Nested case expressions are now translated in a separate check
+  phase rather than during parsing. The data for case combinators
+  is separated from the datatype package. The declaration attribute
+  "case_translation" can be used to register new case combinators:
+
+  declare [[case_translation case_combinator constructor1 ... constructorN]]
+
 * Notation "{p:A. P}" now allows tuple patterns as well.
 
 * Revised devices for recursive definitions over finite sets: