[isabelle-dev] blast

Lawrence Paulson lp15 at cam.ac.uk
Wed Oct 10 15:16:32 CEST 2007

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

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.

More information about the isabelle-dev mailing list