*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Set notation for tuples broken*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 10 Mar 2013 08:39:53 +0100*In-reply-to*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com>*References*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130216 Thunderbird/17.0.3

Am 10/03/2013 00:00, schrieb C. Diekmann: > Hi, > > I want to report that the following set notation is unfortunately not accepted: > {(a,b) ∈ X. P a} > > The following work-around is accepted: > {(a,b). (a, b) ∈ X ∧ P a b} > > lemma split_conv_set: "{x ∈ X. case x of (a,b) ⇒ P a b} = {(a,b). (a, > b) ∈ X ∧ P a b}" > by fastforce > > What must I do to use the first notation? It does not exist is the short answer. It may be possible to modify the syntax to support it, but not as an extension: I would have to modify the basic set syntax. I'll look into it. (In any case, it would only be available as input syntax.) Regards Tobias > Regards > Cornelius >

**References**:**[isabelle] Set notation for tuples broken***From:*C. Diekmann

- Previous by Date: Re: [isabelle] Set notation for tuples broken
- Next by Date: Re: [isabelle] Set notation for tuples broken
- Previous by Thread: Re: [isabelle] Set notation for tuples broken
- Next by Thread: Re: [isabelle] Set notation for tuples broken
- Cl-isabelle-users March 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