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

[Larry Paulson]

Like, next week I do want to try to unify of_nat and real.
Larry

> On 22 Sep 2015, at 15:39, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> I would prefer to leave things as they are now. That print translation is ok and you would be moving the complications elsewhere. We really have more important issues to work on.