[isabelle-dev] blast

[Amine Chaieb]

Hi,
I remarked the following (odd?) behaviour of blast and auto : Although 
they prove the general form:

  ~ P y ==> P x ==> ~ x = y

they can't for the special instance:

  ~ P (0::nat) ==> P x ==> ~ x = 0

I suspect this is due to an implicit classet rule such as
  ~ x = (0::nat) = x > 0.

Is there a simple way to "correct" this behavious, if it might be 
considered erronous?

Cheers,
Amine.