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 present system.


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