*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Indexed Sum/Product Operator*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 04 Dec 2012 20:22:20 +0100*In-reply-to*: <alpine.LNX.2.00.1212041207350.27241@macbroy21.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>*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 12:11, schrieb Makarius: > That is indeed the way and it is not just by luck, because that is an important > principle of the Prover IDE: what you see as formally checked source is > annotated by aspects of the logical content from the prover. So you can explore > it via tooltips or hyperlinks right in the text. > > 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? Tobias

**Follow-Ups**:**Re: [isabelle] Indexed Sum/Product Operator***From:*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

- Previous by Date: Re: [isabelle] nat_code Equation
- Next by Date: Re: [isabelle] Indexed Sum/Product Operator
- Previous by Thread: Re: [isabelle] Indexed Sum/Product Operator
- Next by Thread: Re: [isabelle] Indexed Sum/Product Operator
- 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