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

Larry Paulson lp15 at cam.ac.uk
Tue Sep 22 16:41:19 CEST 2015

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

> 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.

More information about the isabelle-dev mailing list