Hi!
I found out that the pretty-printer for terms in Isabelle do implicitly
beta-normalization and this behavior can't be turned off (in contrast to
eta-normalization).
Is there any serious reason why I can't turn off this feature like in
the case of eta-normalization? It's a bit annoying if you want to do
debugging on the ML level and you have to inspect every term by
inspecting its ML representation (which is really tedious for larger terms).
Thanks for an answer.
Ondrej
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
