Re: [isabelle] refute refutes my simple axiom
On 7/17/2012 4:02 PM, Jasmin Blanchette wrote:
As a general rule, Nitpick subsumes Refute and there is no reason to
use the latter. Refute is provided for historical reasons and might
disappear in a future release. Regards, Jasmin
Jasmin, thanks for the info. I'm happy to simplify my life where possible.
How about quickcheck? Is that something I should forget? I do this:
theorem --"refute finds a model"
"!(x::sT). ~(x ∈⇣σ empty_set)"
And it gives me this:
No active testers for quickcheck
The examples I saw in the list archives didn't give quickcheck any
options, though I tried this, after looking at isar-ref.pdf:
This archive was generated by a fusion of
Pipermail (Mailman edition) and