Re: vocabularies

Freek Wiedijk <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.