*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LaTeXsugar*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Thu, 31 Jan 2013 14:59:34 +0900*In-reply-to*: <1359584222.23351.26.camel@weber>*References*: <510892D9.1010408@gmail.com> <5108C5B9.1020305@in.tum.de> <510925D8.4020404@gmail.com> <51098D9E.3050000@in.tum.de> <1359584222.23351.26.camel@weber>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130110 Thunderbird/17.0.2

On 01/31/2013 07:17 AM, Tjark Weber wrote:

On Wed, 2013-01-30 at 22:16 +0100, Tobias Nipkow wrote:Am 30/01/2013 14:53, schrieb Christian Sternagel:On 01/30/2013 04:03 PM, Tobias Nipkow wrote:I don't like the {f i|i. True} syntax either but your {f i}_i is a bit non-standard, too, isn't it?I don't know ;). I think {f i}_{i : ℕ} is fairly standard,If you can convince me of that, I'll probably add your original syntax (unless other problems crop up). I am just unsure myself, although it looks plausible.I believe {f i}_{i : ℕ} is fairly standard to denote the *sequence* f 0, f 1, f 2, ...; but it does not commonly denote the *set* {f i|i : ℕ}. See, e.g., http://en.wikipedia.org/wiki/Sequence#Indexing In my humble opinion, UN i. {f i} is the better solution. (Also, what about range f?)

http://en.wikipedia.org/wiki/Indexed_family

cheers chris

**References**:**[isabelle] LaTeXsugar***From:*Christian Sternagel

**Re: [isabelle] LaTeXsugar***From:*Tobias Nipkow

**Re: [isabelle] LaTeXsugar***From:*Christian Sternagel

**Re: [isabelle] LaTeXsugar***From:*Tobias Nipkow

**Re: [isabelle] LaTeXsugar***From:*Tjark Weber

- Previous by Date: Re: [isabelle] New error messages in Isabelle 2013
- Next by Date: Re: [isabelle] LaTeXsugar
- Previous by Thread: Re: [isabelle] LaTeXsugar
- Next by Thread: Re: [isabelle] LaTeXsugar
- Cl-isabelle-users January 2013 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