[isabelle-dev] Broken AFP

2016-07-16 Thread Manuel Eberl
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

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

[isabelle-dev] Broken AFP sessions

2015-10-06 Thread Makarius
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