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.
