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

Brian Huffman huffman.brian.c at gmail.com
Wed Apr 24 02:10:43 CEST 2013

I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).

term "(λ(a, b) (c, d). e) x y"

"case_guard True x
  (case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e))))
  :: "'e"

I assume this is a result of the recent changes to the handling of
case expressions?

- 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

More information about the isabelle-dev mailing list