Re: [isabelle-dev] AFP/Lifting_Definition_Option

2015-10-07 Thread Gerwin Klein
The second option has happened now. Cheers, Gerwin > On 8 Oct 2015, at 1:08 am, Ondřej Kunčar wrote: > > This is what I already did when I pushed the upgrade of the lifting package. > I contacted René Thiemann and proposed to make his AFP entry empty except for > a single

Re: [isabelle-dev] Broken AFP sessions

2015-10-07 Thread Dmitriy Traytel
Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is now a simprule). Verified only for the Integral.thy failure. Dmitriy > On 06 Oct 2015, at 23:19, Makarius wrote: > > Here are some more proof failures (Isabelle/5b5656a63bd6 and >

Re: [isabelle-dev] Broken AFP sessions

2015-10-07 Thread Larry Paulson
It’s a bit mysterious. On Monday I got a failure message from the AFP and checked the status page. Four entries were shown as not working. I’ve tried them on my own machine (no matter precisely which version of the sources I had, it certainly had that simprule change, which I had made myself)

Re: [isabelle-dev] AFP/Lifting_Definition_Option

2015-10-07 Thread Ondřej Kunčar
This is what I already did when I pushed the upgrade of the lifting package. I contacted René Thiemann and proposed to make his AFP entry empty except for a single file that would explain what happened. As far as I can remember, he wasn't happy with this solution and proposed to keep the

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

2015-10-07 Thread 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

Re: [isabelle-dev] Broken AFP sessions

2015-10-07 Thread Makarius
On Wed, 7 Oct 2015, Larry Paulson wrote: Now I’ve fixed these too. Great. So in Isabelle/a273bdac0934 and AFP/2351d0b91fb8 everything works, except for the new entry Isabelle_Meta_Model from Isabelle2015. Makarius___ isabelle-dev

Re: [isabelle-dev] Scrollbar, where are thou?

2015-10-07 Thread Makarius
On Tue, 6 Oct 2015, Dmitriy Traytel wrote: I’m not sure if this is rather something for the jEdit mailing list, but I try here first. The attached theory is an empty 500+ lines long file where everything is normal. However, if I add one new line the scrollbar disappears. This is a problem