Re: [isabelle] Problems with nitpick

Hi René,

Am 16.10.2014 um 14:21 schrieb René Thiemann <rene.thiemann at>:

> I just wanted to report a small problem with nitpick:
> lemma "{1, 2} ⊂ - {7,4 :: int}" 
> Nitpick found a counterexample:
> [...]
> There was no weakening indicating like "possibly spurious counter-example",
> so I was surprised by these wrong counter-examples, since actually
> both statements are provable.

Thank you for your bug report. Generally, there was a bug in the handling of the subset operation in the presence of infinite (or otherwise approximated) types. I have fixed the bug and tested the change locally, and will push it (the change) at the next opportunity.



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