[isabelle] Searching in Isabelle



Hello,

I have been working with the type "('a,'b) vec" from HOL-Analysis, and some
AFP entries. Handling such a big library requires searching for various
constructs that other people have built. I've managed to find many things
with the Ctrl+Click feature but there are others that I'd still like to
learn. In particular:

· What's the proper way to find the file where a theorem of the form
"OFCLASS(_,_)" was proved? E.g. how do I find where the type vec was shown
to be a "ring_1"?
· How can I quickly find the line where a notation was introduced? When I
Ctrl+Click the symbol, it takes me to the definition/abbreviation, but the
notation may have been set up in other places.
· If I use a list of "named_theorems" other people introduced, how do I
tell Isabelle to show me the theorem it just applied (from the many
contained in the list)?
· How do I search if a class/locale has been declared a subclass/sublocale
of another?

Sincerely,
Jonathan Julian Huerta y Munive



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.