*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Indexed Sum/Product Operator*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 4 Dec 2012 10:39:46 -0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Johannes Hölzl <hoelzl at in.tum.de>, Lars Noschinski <noschinl at in.tum.de>*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>*Sender*: alfio.martini at gmail.com

Thank you Makarius, Johannes and Lars. It works fine, although if by chance you click first on the symbol and then later press the Control key and then click on the symbol (as I have done many times) it won´t work. You must press Control, then hover the cursor over the symbol and THEN click on the symbol. It took me a while to get it right...:-) Anyway, this functionality is already mentioned in Christian´s small (and nice) tutorial on jEdit. I finally read it. As many others already mentioned here, jEdit is an awesome tool. It makes using Isabelle a completely different experience. It would be great to have a more solid and complete tutorial for the next release. I know that you all work very hard, but I still think that could be a priority amongst the many things that has to be done. Best! On Tue, Dec 4, 2012 at 9:11 AM, Makarius <makarius at sketis.net> wrote: > On Tue, 4 Dec 2012, Johannes Hölzl wrote: > > To find "Setsum" using find_consts or find_theorem is quiet hard as it >> is just a syntax abbreviation and its more general form "∑x∈A. f x" is >> not found when you just search "∑ A". >> >> Luckily with the jEdit interface for Isabelle this gets much easier as >> you can Ctrl-click on the constant and jump to its definition. >> > > 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. > > > Makarius -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**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] Indexed Sum/Product Operator
- Next by Date: [isabelle] Proving set equality -- set-up question
- 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