*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Set notation for tuples broken*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Sun, 10 Mar 2013 08:36:45 +0100*In-reply-to*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com>*References*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com>

When you want to use a pattern in your set comprehension, you can't just write {(a,b). P a b} you have to write: {(a,b) | a b. P a b} 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:*Tobias Nipkow

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

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