[Logiweb] double definition

[Martin Røpcke]

Hi,

I finally found an annoying error making things appear strange. I had 
defined a lemma twice, that is, using the same name two places. The error 
occured due to "copy-paste laziness" and now I have been taught a lesson. 
And besides, searching for the error made my proof a bit more simpel.

So what I did was saying:

"[ math in theory system prime s lemma mendelson proposition...
    says
    peano all...
    end math ]"

and doing it twice.

Anyhow, not remembering much about compiler theory I ask if it isn't 
something that could be caught somewhere by the compiler. Is it possible 
in pyk?

Regards,
Martin