[mizar] MML Query and cscope

[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?

For example, I have the notion of simple group, how can I get the list of
all theorems in the library regarding simple groups?

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.