src/HOL/Set.thy

   by blast
 
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   by blast
 
-lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
-  by blast
-
-lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+  by blast
+
+lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   by blast
 
 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
   by blast
 

   by blast
 
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by blast
 
-lemma Inter_UNIV_conv [iff]:
+lemma Inter_UNIV_conv [simp]:
   "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   by blast+
 
 

 
 lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
   -- {* Look: it has an \emph{existential} quantifier *}
   by blast
 
-lemma UNION_empty_conv[iff]:
+lemma UNION_empty_conv[simp]:
   "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
   "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
 by blast+
 
-lemma INTER_UNIV_conv[iff]:
+lemma INTER_UNIV_conv[simp]:
  "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
  "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
 by blast+
 
 

   by blast
 
 lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
   by (unfold psubset_def) blast
 
-lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
+lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
   by blast
 
 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   by blast