*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Indexed Sum/Product Operator*From*: Makarius <makarius at sketis.net>*Date*: Tue, 4 Dec 2012 12:11:54 +0100 (CET)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Alfio Martini <alfio.martini at acm.org>*In-reply-to*: <1354608091.3991.27.camel@localhost.localdomain>*References*: <CAAPnxw34ziFh_AjQwWN8UKcVeB+OkutvYPpPa8gdiDVZurHPvA@mail.gmail.com> <1354608091.3991.27.camel@localhost.localdomain>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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.

Makarius

**Follow-Ups**:**Re: [isabelle] Indexed Sum/Product Operator***From:*Alfio Martini

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

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

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

- 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