In the past few months/weeks/days certain issues of interrupts and
timeouts (which are based on interrupts internally) have emerged in
private mail conversations with several people.
Recently David Matthews has kindly clarified some extreme corner cases, so
I've made another round to robustify this on our side, e.g. see the
vicinity of 82339c3fd74a.
There are still some pending questions concerning interactive "auto"
checking tools, though. I've first thought that this could be related,
but the reasons might be much more profane. (The above-mentioned corner
cases of Poly/ML interrupts are so extreme, that they might not have shown
up in practice so far.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
