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)))) case_nil) y" :: "'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 <tray...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev