[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,

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