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