[isabelle-dev] Possible non-determinism in HOL-ODE-Numerics

Makarius makarius at sketis.net
Sat May 12 00:44:29 CEST 2018

On 11/05/18 14:12, Lars Hupel wrote:
>> Last known good state is:
>> Isabelle/7e349d1e3c95
>> AFP/c3cfeceda7a0
> We're back to normal now, as of
> Isabelle/58c9231c2937
> AFP/79f64c92d5ae

Great. I had already started some experiments, but they were inconclusive.

Just for the record, the relevant point seems to be

changeset:   9230:b0febe244fbc
user:        paulson <lp15 at cam.ac.uk>
date:        Fri May 11 12:12:01 2018 +0100
fix to nonterminating proof


More information about the isabelle-dev mailing list