*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Set notation for tuples broken*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Tue, 12 Mar 2013 13:04:52 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <513EDD64.2000903@in.tum.de>*References*: <CAGbqCMyua4OKBLRe0DvZvNTMUD+AEeMCVteBy8Rfz48ioj-QbA@mail.gmail.com> <513EDD64.2000903@in.tum.de>*Sender*: c.diekmann at googlemail.com

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? Cheers Cornelius

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

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

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

- Previous by Date: Re: [isabelle] Transfer rule for transfer_forall
- Next by Date: [isabelle] Completeness of patterns for mutually recursive function definitions
- 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