[isabelle-dev] implicit beta normalization in the pretty-printer

Ondřej Kunčar 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 mailing list