# Re: [isabelle] Indexed Sum/Product Operator

On Tue, 4 Dec 2012, Tobias Nipkow wrote:

`Sometimes these "aspects" are still missing or only approximative, but
``the coverage is increasing over time. So the need for separate
``diagnostic commands like find_consts is more and more diminished.
`

`The interesting part of the functionality of find_consts is search by a
``given type (a bit like Hoogle, if you speak Haskell). How do you plan to
``replace that by tooltips and hyperlinks?
`

`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.)
`

`In contrast, the application sketched in this thread, you have your formal
``(con)text where you presently work already.
`

`In the past query tools like find_theorems were often re-used to explore
``the local proof context, but this can be done more directly. Similarly
``replacement of interactive diagnostics can be anticipated for print_cases,
``print_facts, "thm calculation", "thm this" etc.
`

`"Big" IDEs for Java do such things routinely. That is conceptually not
``such a big deal, and no need to go back to TTY-style commands.
`
Makarius

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