[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] definitions, vocabularies, and findvoc
Hi,
On Tue, 15 Feb 2005, Jesse Alama wrote:
> What explains the difference between Fixed and Free? Why is QC_LANG3
> mentioned in the output of `findvoc Fixed' but not in the output of
> `findvoc Free'?
The findvoc utility reports the contents of *.voc files that the authors
contribute with their articles when they want to introduce new symbols.
But in case a symbol has been introduced by someone else before (here
'Free' belongs to the vocabulary ZF_MODEL), the symbol is not
re-introduced in a new vocabulary. So there is no direct correspondence
between the symbols used for objects defined in an article and its
vocabulary file. In consequence, browsing the vocabularies with findvoc or
listvoc is not intended to be a reliable way of finding definitions using
given symbols. If you use the Emacs mode for Mizar, "View symbol def" is
the preferred way to do it. Otherwise you are left with grepping the
abstracts.
Best regards,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================