Re: [mizar] Re: Mizar Parser

[Freek Wiedijk <freek@cs.kun.nl>]

Grzegorz:

>MML Query can be downloaded. It is a bunch of perl scripts
>plus 1Gb of data.

1Gb!  That's a lot!  Why is it so big?  I'd hate to have to
download that for each new version of MML!

>The names of items can be found in  Mizar eXtended Abstracts
>  http://megrez.mizar.org/pub/mxa/

Are those mxa's available in just one tar.gz file?  And is
there a set of ".mxa.html" files that contain hyperlinks,
like the jfmabstr.tar.gz?

>Now, there is no usable description of MML Query system.

Is there a list of example queries?  I think that's all you
need to understand how to use it?

>You can get there full info of a statement in any place of
>mizar article.

I don't understand this.  Suppose I'm in emacs in an article
I'm writing, I'm in some formula (say "f.(-x) = -f.x"), and
want to know the constructors of that formula (because I want
to know the constructor of the "-").  Now what do I do?

Freek