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

[Brian Huffman]

It would be nice to get HOLCF case combinators working with this new
system, as the parsing for HOLCF case expressions has been a bit
broken for some time.

Can case combinators and constructor functions with
continuous-function types be made to work with the "case_tr" (or
"case_translation"?) attribute? Even if we need a separate
HOLCF-specific attribute, might it be possible to get HOLCF case
expressions to work with the new translation check phase?

- Brian

On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel <traytel at in.tum.de> wrote:
> * 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev