Re: [isabelle] Indexed Sum/Product Operator

Thank you Makarius, Johannes and Lars.

It works fine, although if by chance you click first on the symbol and then
press the Control key and then click on the symbol (as I have done many
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
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.


On Tue, Dec 4, 2012 at 9:11 AM, Makarius <makarius at> 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

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