On 31/05/18 16:36, Makarius wrote: > > Anyway, with approx. 100min CPU time HOL-ODE-Numerics has become > eligible for the "AFP slow" category: paradoxically this will make the > test much faster, but also less accurate in its timing information, > because the test hardware and settings are quite different.
Several sessions depend on HOL-ODE-Numerics: HOL-ODE-Examples, Lorenz_Approximation, Lorenz_C0, Lorenz_C1 So it is better to keep it as non-slow: otherwise the whole tower needs to be moved. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev