[isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]

[Makarius]

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