Re: [mizar] vocabularies

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Andrzej,

>What is on foo.voc is often accidental.

The location of _almost everything_ in MML is often
accidental.  If you consider this a serious issue then you
should move around stuff in MML much more than currently
happens.

>After a revision the definitions of the attributes were
>moved to XXREAL_0. But symbols are still on old
>vocabularies.

That's a bad argument: just move the symbols also to XXREAL_0
(or to yet another article if that's a more natural place
for them).  Sorry, but I don't see the point of this example.

>What I have in mind that (without preprocessing) we should
>move symbols from one article to the other, any time we
>change the order of processing.

I would expect this to be minor.  Doesn't this kind of
thing also happen with definitions and notations and so on?
It seems more of the same.

Freek