Hi Andreas, thanks, you're making some good points.
> Testing quickcheck is indeed quite tricky. Do you know which of the > quickcheck calls time out? Does it happen only with the random generator > or also with exhaustive? No, it fails on all of them. > It might be that you have a fairly large set of code equations and the > timeout already kicks in during code generation or compilation with > PolyML, though. A larger timeout should help there. > > Moreover, both statements have two free variables and you rely on the > quickcheck generators being able to quickly come up with two different > values for them. If you are not to set on the property, you could > alternatively use > > lemma "x ~= x" for x :: dec > > which will definitely fail on the first generated example. I'll apply both changes, in the hope that it makes it more robust. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
