[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] vocabularies

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