[Logiweb] double definition

[Klaus Ebbe Grue]

Hi Martin,

> 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.

I suppose this is a follow up on [Logiweb] lemma proof mismatch.

If the pyk compiler sees that the same aspect of the same construct is 
defined more than once, it compares the right hand sides of the 
definitions and, if they differ, print a warning.

In particular, if a lemma is stated twice, the compiler prints a warning 
unless the two instances are completely identical.

But the warning hides in the horrible amounts of output from the compiler. 
Some day I think I choke the output from TeX. That should reduce the 
amount of output to a level where it makes sense to spot warnings (but one 
will risk to miss TeX warnings, of course).

Klaus