1.1 --- a/src/HOL/Set.thy	Mon Aug 23 09:04:37 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Aug 23 11:56:30 2010 +0200
     1.3 @@ -852,7 +852,7 @@
     1.4  lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
     1.5    by blast
     1.6  
     1.7 -lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
     1.8 +lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
     1.9    -- {* This rewrite rule would confuse users if made default. *}
    1.10    by blast
    1.11  
    1.12 @@ -1203,7 +1203,7 @@
    1.13  lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
    1.14    by (fact inf_eq_top_iff)
    1.15  
    1.16 -lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
    1.17 +lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
    1.18    by (fact le_inf_iff)
    1.19  
    1.20  lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
    1.21 @@ -1294,7 +1294,7 @@
    1.22  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
    1.23    by (fact sup_eq_bot_iff)
    1.24  
    1.25 -lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    1.26 +lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    1.27    by (fact le_sup_iff)
    1.28  
    1.29  lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
    1.30 @@ -1490,7 +1490,7 @@
    1.31  lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
    1.32    by blast
    1.33  
    1.34 -lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
    1.35 +lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
    1.36    by blast
    1.37  
    1.38  lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"