*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Set notation for tuples broken*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Sun, 10 Mar 2013 00:00:56 +0100*Sender*: c.diekmann at googlemail.com

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

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

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

- Previous by Date: Re: [isabelle] Easily using built-in tactics at the ML level (and/or using a method as a tactic)
- Next by Date: Re: [isabelle] Set notation for tuples broken
- Previous by Thread: Re: [isabelle] Updating to a previous Document.Version using Isabelle/Scala
- 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