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)"
quickcheck

And it gives me this:

Quickchecking...
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:

quickcheck [exhaustive]

Thanks,
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.