[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] MML duplications

On Tue, Jul 29, 2008 at 02:52:30AM +0200, Josef Urban wrote:
> 
> On Mon, 28 Jul 2008, Jesse Alama wrote:

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

> There are quite a few situations like that, my conjecture is that this is 
> done to keep the theorem numeration stable.

Maintaining the numbering of theorems stable (if this is the case)
leeds to fossilization of MML.  What is the problem in renumbering theorems
after moving them around?  Renumbering all theorems and references in MML
after a revision seems like a mundane editorial job.

One argument that I see in support for avoiding renumbering theorems is that
authors get used to numbers of frequently referenced theorems.  This does not
apply to me; I have to look at the referenced theorems all the time ;-)

Cheers,

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr