Re: [mizar] A revision

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Wed, 26 Nov 2003, Piotr Rudnicki wrote:

> I am finishing the proof of the finite skew-field Weddernburn theorem
> and I need to use stuff from POLYNOM4 and POLYNOM5 on univariate
> polynomials.  Robert Milewski has proven some facts that I need
> requiring that the coefficients are from a Field-like structure where
> domRing (integral domain) would suffice.  Shall I continue using
> Field-like, or revise POLYNOM4 and POLYNOM5, or maybe steal Robert's theorems
> and generalize them?

My experience is that it is preferable to revise the articles, and use 
them locally (putting them in your local prel), until your main article is 
finished.
If it is an obvious improvement, there should be no problems with the 
Library Committee afterwards - the only problem is, when some 
other revision is done in the meantime on the articles. 

The MMLCVS could make this easier for the Committee - if 
some user branches were allowed, the mergings could be more automated and 
more incremental. It would also allow to keep track of the authors of the 
revision changes, motivating the authors to improve the existing 
articles, rather than produce new articles by copy&edit, which often 
pollutes the library.

> I guess that the revision of the past is the way to go.  I am sure
> that if the MML submissions were reviewed before inclusion then many
> such issues would have been caught early and thus there would be no
> need for some revisions of the past.  

I agree that reviewing can do a lot, but sometimes you only need a 
small part of some theory in your article, and do not care about the 
theory as a whole and in its full generality, and then someone else
may care, and starts from generalizing it. So there will probably always 
be need for revisions.

Best,
Josef