Re: vocabularies
Freek Wiedijk <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
Hi Josef, >>To me this seems a much more drastic change than what I >>was proposing. I guess it also would mean unifying the >>vocabulary and article name spaces? > >I think there would be no "vocabulary". So all vocabularies would be always active? But then I could break existing articles by introducing new symbols in my vocabulary to MML. So how should I test for that? Or would you want to introduce the vocabulary elements together with the notation, always? So that sounds a more radical change than what I proposed. (My proposal was just to move text from one file to another, but without the system really changing.) Freek