[isabelle-dev] Isabelle2013-2 release

[Tobias Nipkow]

Am 20/11/2013 22:49, schrieb Makarius:
> Are there any other potential problems of Isabelle2013-1 that were not reported
> yet?

There is a problem with autoquickcheck in Isabelle/jedit. It sometimes fails to
find or dislay a counterexample. I have a theory with a wrong lemma in it. When
I load the theory, no counterexample is displayed. When I edit the theory such
that that lemma needs to be rechecked, suddenly the counterexample is found.
Afterwards it is always found reliably. The first time is the difficult time.

This is not easy to reproduce: if you just use "False" or "x=x", it will find a
counterexample reliably. I have tried to create a short example but failed. I
have noticed this some time ago, but was never sure if it was just a fluke. Now
I have a collection of theories where it reproduces reliably.

Tobias