src/HOL/Set.thy
changeset 67091 1393c2340eec
parent 67051 e7e54a0b9197
child 67268 bdf25939a550
     1.1 --- a/src/HOL/Set.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -837,7 +837,7 @@
     1.4  lemma subset_Diff_insert: "A \<subseteq> B - insert x C \<longleftrightarrow> A \<subseteq> B - C \<and> x \<notin> A"
     1.5    by blast
     1.6  
     1.7 -lemma doubleton_eq_iff: "{a, b} = {c, d} \<longleftrightarrow> a = c \<and> b = d \<or> a = d & b = c"
     1.8 +lemma doubleton_eq_iff: "{a, b} = {c, d} \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
     1.9    by (blast elim: equalityE)
    1.10  
    1.11  lemma Un_singleton_iff: "A \<union> B = {x} \<longleftrightarrow> A = {} \<and> B = {x} \<or> A = {x} \<and> B = {} \<or> A = {x} \<and> B = {x}"
    1.12 @@ -1584,7 +1584,7 @@
    1.13    "\<And>A P Q. (\<exists>x\<in>A. P \<and> Q x) \<longleftrightarrow> (P \<and> (\<exists>x\<in>A. Q x))"
    1.14    "\<And>P. (\<exists>x\<in>{}. P x) \<longleftrightarrow> False"
    1.15    "\<And>P. (\<exists>x\<in>UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
    1.16 -  "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a | (\<exists>x\<in>B. P x))"
    1.17 +  "\<And>a B P. (\<exists>x\<in>insert a B. P x) \<longleftrightarrow> (P a \<or> (\<exists>x\<in>B. P x))"
    1.18    "\<And>P Q. (\<exists>x\<in>Collect Q. P x) \<longleftrightarrow> (\<exists>x. Q x \<and> P x)"
    1.19    "\<And>A P f. (\<exists>x\<in>f`A. P x) \<longleftrightarrow> (\<exists>x\<in>A. P (f x))"
    1.20    "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"