[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] MML duplications
Very interesting and rich material. We should use it to revise MML, of
course. However the value of information varies.
The most important are true repetition, i.e. the same kind of the item.
So we have three duplications of definitions (actually one in POLYEQ_3,
two remaining are redefinitions that do not changed the meaning). 24
functor registrations.
I work on a revision so I have removed repeated definitions, and 20
functor registrations. It caused some changed
in the Environment Declaration of depeding articles, nothimg serious.
At least one functor registration had been already removed (I mean the
duplication of it).
Josef,
it is very useful and very important utility. How to use it:
1. I would like it to be called after every revision (good chances that
new repetitions happen).
2. It would be useful tool for reviewers, or for the Athors if they
would rather avoid problems with reviews.
Could be it distributed with Mizar? How long it runs?
Regards,
Andrzej
Josef Urban wrote:
Hi,
at http://octopi.mizar.org/~urban/dupl.html is a list of more than
1000 MML duplications.
Josef