Hallo,
sorry for the broken AFP – it's my fault, but I added a lot of new
material about rings and prime factor decomposition. The projects that
were affected by this the most are already fixed, and I will take care
of the rest on Monday.
Manuel
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)
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
Here are some more proof failures (Isabelle/5b5656a63bd6 and
AFP/21bdf9fbf229):
Integration FAILED
*** At command "by" (line 1724 of
"~/isabelle/afp-devel/thys/Integration/Integral.thy")
Markov_Models FAILED
*** At command "done" (line 1038 of