Re: [mizar] MML duplications

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> at http://octopi.mizar.org/~urban/dupl.html is a list of more than
> 1000 MML duplications.

How many of these are caused by the fact that, in some articles, some
authors prove results without "exporting" them using the theorem
keyword?  It is frustrating to find out, after looking for a theorem in
the MML, that it is off-limits to you because the author thought that a
result should be just a lemma rather than a theorem.  (Down with lemmas,
I say!  Make every proved result available to everyone, not just
yourself.)

Lemmas can even lead to odd situations such as Lm1 in ZFMISC_1 and
ZFMISC_1:37.

Jesse

-- 
Jesse Alama (alama@stanford.edu)