On Tue, 22 Sep 2015, Florian Haftmann wrote:
The situation turned out more complicated than anticipated: implicit
eta-contraction happens at a rather late level in the printing machinery
using a print translation. Hence, any countermeasure must act on the
same (or a later level). However in the ecosystem as it is today, it
seems better to do such transformations at the uncheck level, i.e. quite
close to the logic.
The uncheck phase -- despite being introduced already in 2006/2007 -- is
not fully used as much as it could or should. Apart from eta contraction,
there are other fine points that I don't dare to dig up at the moment.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
