Re: [mizar] MML Query and cscope

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

Quoting mnf72 <aliptah@gmail.com>:

> Dear all,
>
> time ago when I programmed I used a tool called cscope. I basically used
> just two functions: the first was to 'jump' to the text defining a function
> of a given name, the second was to get all the definitions of the functions
> that used a given function.
> Now, in mathematics, I still want to do these two base operations: 1.
> jumping, which is already available from the html interface of a Mizar
> article, and 2. the inverse of jump. (you could call them 'zooming in' and
> 'zooming out')
>
> Then the MML Query question is: given a constructor/substring/theorem X how
> can I get the list of all theorems that 'use' X?

Actually, you cannot get such info because spelling of
variables is not stored. Important is type of variable.
> For example, I have the notion of simple group, how can I get the list of
> all theorems in the library regarding simple groups?

list of th where [ref and {simple_group}]
or
simple_group | th

where simple_group in MMLQuery name.

If you don't know MMLQuery name you may just type Mizar symbol
e.g. the_normal_subgroups_of
in query frame in httpL//mmlquery.mizar.org/mmlquery/three.html


> I read the MML Query examples documentation, but it is really too abstruse
> (I am not a real mizar user, but I have seen that MML is quite readable if
> you already know what you are reading).
>
> So, could you give me some MML Query expressions to solve the matter?
>
> Many thanks.
>
> Best regards,
> Andrea
> --
> View this message in context: 
> http://old.nabble.com/MML-Query-and-cscope-tp32998572p32998572.html
> Sent from the Mizar mailing list archive at Nabble.com.

Grzegorz