[isabelle] Problems with nitpick



Dear all,

I just wanted to report a small problem with nitpick:

lemma "{1, 2} ⊂ - {7,4 :: int}" 
Nitpick found a counterexample:

  Empty assignment


lemma "{1, 2} ⊂ - {7,4 :: int} ∪ {x}" 
Nitpick found a counterexample:

  Free variable:
    x = 1


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.

Kind regards,
René






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