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.
[
Home |
Project |
Language |
System |
People |
MML |
FM |
SUM
]
Last modified: October 28, 2014
Please contact our
Webmaster
with other questions or comments.