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