Re: [mizar] vocabularies

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

Hi Josef,

>yes; I think something really should be done with the
>environment "black magic";

I agree.  I also think that given the current Mizar culture,
it just won't happen.

If even my very modest proposal to integrate the vocabulary
files into the articles is seen as a huge problem for
maintaining the MML (it isn't!) even bigger changes do not
stand any chance of happening.  I fear.

>perhaps even the "constructors" directive could be made only
>optional or removed totally;

I especially am always very surprised by the "theorems"
directive.  Certainly it only needs an utterly trivial pass
over the article to find out what should go in there.

I often need to run Mizar twice because I forgot to add an
article to the theorem directive.  That is a serious pain
in the you-know-where.

Freek