Re: [isabelle] Set notation for tuples broken



Am 10/03/2013 00:00, schrieb C. Diekmann:
> 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?

It does not exist is the short answer. It may be possible to modify the syntax
to support it, but not as an extension: I would have to modify the basic set
syntax. I'll look into it. (In any case, it would only be available as input
syntax.)

Regards
Tobias

> Regards
>   Cornelius
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.