Re: [mizar] vocabularies

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Mon, Jan 05, 2009 at 07:48:58PM +0100, Freek Wiedijk wrote:

> 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. ...

I support Freek.  Is the extra pass even needed?  Can the import
of theorems be done on the fly?

On the other hand, it is interesting what was the past motivation for
introducing the theorems directive.  (With the schemes directive the
story is different).

Best,

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr