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

Dmitriy Traytel traytel at in.tum.de
Wed Apr 10 18:16:29 CEST 2013

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

This refers to Isabelle/bdaa1582dc8b


More information about the isabelle-dev mailing list