*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Indexed Sum/Product Operator*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 05 Dec 2012 08:09:37 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1212042051260.6945@macbroy20.informatik.tu-muenchen.de>*References*: <CAAPnxw34ziFh_AjQwWN8UKcVeB+OkutvYPpPa8gdiDVZurHPvA@mail.gmail.com> <1354608091.3991.27.camel@localhost.localdomain> <alpine.LNX.2.00.1212041207350.27241@macbroy21.informatik.tu-muenchen.de> <50BE4D6C.704@in.tum.de> <alpine.LNX.2.00.1212042051260.6945@macbroy20.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:17.0) Gecko/17.0 Thunderbird/17.0

Am 04/12/2012 20:58, schrieb Makarius: > 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.) I was not talking of the search facility itself (as Gerwin noted, we have a number of nifty tools beside find_const) but how to invoke it without having to type the command name. Command completion is already nice, but still crude. Because the name can be nondescriptive and the parameters unclear. An example of what I mean: Larry was not aware of the type-based search via find_consts. Contrast this with the nice box that cmd-f gives you in many tools, eg jedit. Tobias > 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

**References**:**[isabelle] Indexed Sum/Product Operator***From:*Alfio Martini

**Re: [isabelle] Indexed Sum/Product Operator***From:*Johannes Hölzl

**Re: [isabelle] Indexed Sum/Product Operator***From:*Makarius

**Re: [isabelle] Indexed Sum/Product Operator***From:*Tobias Nipkow

**Re: [isabelle] Indexed Sum/Product Operator***From:*Makarius

- Previous by Date: [isabelle] Launch of Elbe 1.63
- Next by Date: Re: [isabelle] Indexed Sum/Product Operator
- Previous by Thread: Re: [isabelle] Indexed Sum/Product Operator
- Next by Thread: [isabelle] Proving set equality -- set-up question
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list