*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LaTeXsugar*From*: Tjark Weber <webertj at in.tum.de>*Date*: Wed, 30 Jan 2013 23:17:02 +0100*In-reply-to*: <51098D9E.3050000@in.tum.de>*References*: <510892D9.1010408@gmail.com> <5108C5B9.1020305@in.tum.de> <510925D8.4020404@gmail.com> <51098D9E.3050000@in.tum.de>

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?) Best regards, Tjark

**Follow-Ups**:**Re: [isabelle] LaTeXsugar***From:*Christian Sternagel

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

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

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

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

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

- Previous by Date: Re: [isabelle] New error messages in Isabelle 2013
- Next by Date: [isabelle] Using ISABELLE_BUILD_OPTIONS in Isabelle 2013
- 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