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 mailing
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) an
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
> AFP/21bdf9fbf229):
>
> Integration
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
"~/isabelle/afp-devel/thys/Markov_Models/Classify