Re: [isabelle] Indexed Sum/Product Operator
On Tue, 4 Dec 2012, Gerwin Klein wrote:
This is just a different category of application: search over a
"mathematical" library, and really good solutions to that are still
missing. (I am occasionally attending the MKM conference, where people
are discussing that.)
I think that the combination of tooltips/hover links and the existing
searches in find_theorems and find_consts is actually pretty good for
searching our fact base (think back 10 years when grep was the power
tool of choice).
Grep would be "hypersearch" in jEdit, and I am using this a lot. It could
be improved to take the semantic markup into account: search for regular
expressions relative to some XML path context.
Things can and should certainly be improved, but I wouldn't diminish one
kind of tool over the other. Both have their place.
The start of the thread was a confusion about the right tool to use for
the job. What you see already formally in your bit of theory or an
example by someone else does not have to be queried again, it is already
there to be explored.
I have recently brushed up the "find" tools a bit to provide more
hyperlinks in their output for the coming release, such that they can
participate in the game better. Much more could and should be done there,
to get them to the state of the art of potential possibilities of the
This archive was generated by a fusion of
Pipermail (Mailman edition) and