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