Re: vocabularies

trybulec <[email protected]> Tue, 06 Jan 2009 19:21:50 +0100

Newsgroups	gmane.comp.mathematics.mizar
Message-ID	<[email protected]>

Piotr Rudnicki wrote:

> <>On Mon, Jan 05, 2009 at 07:48:58PM +0100, Freek Wiedijk wrote:
>
> 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).
>
You should remember. A mispelling of a reference to a theorem more often 
happens than
the need of adding  the name of theorems file to the 'theorems' directive.

Maybe more important is that you should first run PARSER (for the Text 
Proper), to generate
a file for the ACCOMMODATOR (maybe incorrect) and then to run the 
VERIFIER. Clumsy.

Regards,
Andrzej