On 02/09/18 16:00, Manuel Eberl wrote: > Okay I did some more experiments and I was now, interestingly enough, > completely unable to reproduce the situation where Green /didn't/ > timeout. So I have no idea what was going on there; perhaps I made a > mistake in testing it. I don't know. > > It might be wise to remove "continuous_on_discrete" etc. from > intro/continuous_intros and declare it as a simp rule instead. I'm still > not quite sure what causes these problems.
The official isabelle-dev test results show that Ergodic_Theory and Lp have suffered a lot: https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Ergodic_Theory https://isabelle.sketis.net/devel/build_status/AFP/index.html#session_Lp Here are some manual measurements: Isabelle/9207ada0ca31 + AFP/6d7e0f6b8096 Finished HOL (0:03:18 elapsed time, 0:11:01 cpu time, factor 3.33) Finished HOL-Analysis (0:05:44 elapsed time, 0:26:07 cpu time, factor 4.55) Finished HOL-Probability (0:01:15 elapsed time, 0:05:25 cpu time, factor 4.30) Finished Lp (0:00:15 elapsed time, 0:01:03 cpu time, factor 4.21) Isabelle/f443ec10447d + AFP/6d7e0f6b8096 Finished HOL (0:03:19 elapsed time, 0:11:03 cpu time, factor 3.33) Finished HOL-Analysis (0:05:58 elapsed time, 0:27:06 cpu time, factor 4.54) Finished HOL-Probability (0:01:16 elapsed time, 0:05:24 cpu time, factor 4.22) Finished Lp (0:02:41 elapsed time, 0:03:42 cpu time, factor 1.38) So it is probably better to revise the rule declarations in main HOL. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev