[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

> I think it works properly now, see Isabelle/f0f83ce0badd + AFP/f7e9efc65d82.

Thanks for that. I'll proceed with the systems integration process of
that machine now.

> I usually measure the CPU time, multiply it by 2, and take the ceiling
> towards the next multiple of 300. In principle this maintenance of
> options could be automated.

The "multiple of 300" part is now implemented in "afp_check_roots"
(AFP/006f6826c3a1).

Cheers
Lars