src/HOL/Set.thy
 changeset 18447 da548623916a parent 18423 d7859164447f child 18674 98d380757893
     1.1 --- a/src/HOL/Set.thy	Tue Dec 20 22:06:00 2005 +0100
1.2 +++ b/src/HOL/Set.thy	Wed Dec 21 12:02:57 2005 +0100
1.3 @@ -1452,10 +1452,10 @@
1.4  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
1.5    by blast
1.6
1.7 -lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
1.8 +lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
1.9    by blast
1.10
1.11 -lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
1.12 +lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
1.13    by blast
1.14
1.15  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
1.16 @@ -1479,7 +1479,7 @@
1.17  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
1.18    by blast
1.19
1.20 -lemma Inter_UNIV_conv [iff]:
1.21 +lemma Inter_UNIV_conv [simp]:
1.22    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
1.23    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
1.24    by blast+
1.25 @@ -1555,12 +1555,12 @@
1.26    -- {* Look: it has an \emph{existential} quantifier *}
1.27    by blast
1.28
1.29 -lemma UNION_empty_conv[iff]:
1.30 +lemma UNION_empty_conv[simp]:
1.31    "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
1.32    "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
1.33  by blast+
1.34
1.35 -lemma INTER_UNIV_conv[iff]:
1.36 +lemma INTER_UNIV_conv[simp]:
1.37   "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
1.38   "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
1.39  by blast+
1.40 @@ -1790,7 +1790,7 @@
1.41  lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
1.42    by (unfold psubset_def) blast
1.43
1.44 -lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
1.45 +lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
1.46    by blast
1.47
1.48  lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"