*To*: "C. Diekmann" <diekmann at in.tum.de>*Subject*: Re: [isabelle] Set notation for tuples broken*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 13 Mar 2013 07:55:56 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAGbqCMxmY0o09QA5jCQKcgQZpB80QucTsYo_F8m85Fn=6saWmg@mail.gmail.com>*References*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com> <513EDD64.2000903@in.tum.de> <CAGbqCMxmY0o09QA5jCQKcgQZpB80QucTsYo_F8m85Fn=6saWmg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130307 Thunderbird/17.0.4

Am 12/03/2013 13:04, schrieb C. Diekmann: > 2013/3/12 Tobias Nipkow <nipkow at in.tum.de>: >> Am 10/03/2013 00:00, schrieb C. Diekmann: >>> I want to report that the following set notation is unfortunately not accepted: >>> {(a,b) ∈ X. P a} >> >> Now it is, in the development version. It is input syntax that tranlates into >> {(a,b). (a,b) ∈ X & P a}. >> > > Great :) > > I guess the lemma I called split_conv_set might be also very useful > for the simplifier then? I don't see that it would help much. Tobias > Cheers > Cornelius >

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

**Re: [isabelle] Set notation for tuples broken***From:*Tobias Nipkow

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

- Previous by Date: [isabelle] syntax highlighting on stackoverflow
- Next by Date: [isabelle] Induction rule for partial_function (tailrec)
- Previous by Thread: Re: [isabelle] Set notation for tuples broken
- Next by Thread: [isabelle] Transfer rule for transfer_forall
- 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