[isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

[Dmitriy Traytel]

* 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_tr" can be used to register new case combinators:

   declare [[case_translation case_combinator constructor1 ... 
constructorN]]

This refers to Isabelle/bdaa1582dc8b

Dmitriy