--- 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.
--- 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: