Re: vocabularies

Dear Andrzej,

>The "big" difference is in the fact that I am not pressed
>to move a symbol to another vocabulary if I changed the
>order of processing.

Okay, I see the point now.  Although this seems to me is
not something that would happen very often?  Also, the same
thing already happens with the notations and registrations,
I guess.  So it just seems to be a little bit more of the
same thing?

>Merry Christmas,

Thanks, my best wishes to you too.  And to all other Mizar
users around the world!

Freek