Re: [mizar] definitions, vocabularies, and findvoc

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

Hi,

On Wed, 16 Feb 2005, Adam Naumowicz wrote:

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

You may also ask MML Query
(http://merak.pb.bialystok.pl/mmlquery/three.html)

/Free/

and get all 5 definition using this symbol.

Grzegorz


===============================================================
Grzegorz Bancerek
e-mail: bancerek@mizar.org (bancerek@math.uwb.edu.pl)
http://merak.pb.bialystok.pl/~bancerek/
Dept. of Theoretical CS
Faculty of Computer Science      fax. +48 (85) 746-9057
Bialystok Technical University   tel. +48 (85) 746-9056
http://www.pb.bialystok.pl