[isabelle] Set notation for tuples broken


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?


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