Re: [isabelle] Indexed Sum/Product Operator



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


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