Re: [isabelle] Set notation for tuples broken



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




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