[isabelle-dev] blast

[Lawrence Paulson]

I'm sure you are right. We could try taking it out, though I suspect  
this will break many proofs.
Larry

On 10 Oct 2007, at 12:03, Tobias Nipkow wrote:

> I have had problems with the conversion from ~ x = (0::nat) to x >  
> 0 as
> well. Can anyone recall why we installed that? I suspect it may have
> helped a little before we had linear arithmetic but I now feel it is
> more of a problem than a solution. Maybe I'm missing something.