Revisions of the Mizar Mathematical Library

The Mizar Mathematical Library is quite frequently revised. There are different kinds of revisions:

• an authored revision consists of small changes in some articles in the library when somebody writing a new article notices a theorem or a definition in an old article that can be generalized. When this generalization is done, sometimes it is necessary to change (or possibly improve) some older articles that depend on the change. As a rule, a small part of the library is affected.
• an automatic revision takes place frequently whenever either a new revision software is developed, (e.g. software for checking equivalence of theorems, which enables to remove one or two equivalent theorems) or the Mizar verifier is strengthened and existing revision programs can use it to simplify articles.
• a reorganization of the library is rare, but it happens. It consists in changing the order of processing articles when the Mizar Data Base is created.