[isabelle-dev] HOL-ODE-Numerics vs. HOL-ODE-Refinement

[Makarius]

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