*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 09:45:43 +0100*In-reply-to*: <28C5331F-F274-4FD7-9185-913E1C879AB0@cam.ac.uk>*References*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com> <28C5331F-F274-4FD7-9185-913E1C879AB0@cam.ac.uk>*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 08:36, schrieb John Wickerson: > When you want to use a pattern in your set comprehension, you can't just write > > {(a,b). P a b} Yes, you can. It stands for Collect(%(a,b). P a). > you have to write: > > {(a,b) | a b. P a b} This produces Collect(%p. EX a b. p = (a,b) & P a b). Tobias > cheers, > john > > On 10 Mar 2013, at 00:00, C. Diekmann wrote: > >> 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? >> >> Regards >> Cornelius >> >

**Follow-Ups**:**Re: [isabelle] Set notation for tuples broken***From:*John Wickerson

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

**Re: [isabelle] Set notation for tuples broken***From:*John Wickerson

- 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