[isabelle-dev] implicit beta normalization in the pretty-printer
kuncar at in.tum.de
Wed Jan 18 15:34:35 CET 2012
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
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.
More information about the isabelle-dev