Re: [isabelle] Set notation for tuples broken



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
> 




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