Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Set notation for tuples broken

Email Gateway (Aug 19 2022 at 10:41):

From: "C. Diekmann" <diekmann@in.tum.de>
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?

Regards
Cornelius

Last updated: Nov 21 2024 at 12:39 UTC