Re: [isabelle] refute refutes my simple axiom



Am 17.07.2012 um 23:31 schrieb Gottfried Barrow:

> 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?

If you use "axiomatization", yes. Quickcheck requires executable definitions / code equations.

Jasmin






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