Re: [isabelle] Set notation for tuples broken

2013/3/12 Tobias Nipkow <nipkow at>:
> 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?


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