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