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 <makar...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
