[isabelle-dev] Broken AFP sessions

[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 <makarius at sketis.net> wrote:
> 
> 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/Classifying_Markov_Chain_States.thy")
> *** At command "by" (line 1077 of "~/isabelle/afp-devel/thys/Markov_Models/Classifying_Markov_Chain_States.thy")
> 
> Ordinary_Differential_Equations FAILED
> *** At command "by" (line 804 of "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")
> *** At command "by" (line 704 of "~/isabelle/afp-devel/thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy")
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev