# HG changeset patch
# User blanchet
# Date 1282557390 -7200
# Node ID 52ea97d95e4bed5194a156571377b50b576e0143
# Parent  5500241da479f08685697ca4796c3a4a3f0e79a3
"no_atp" a few facts that often lead to unsound proofs

diff -r 5500241da479 -r 52ea97d95e4b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Aug 23 09:04:37 2010 +0200
+++ b/src/HOL/Set.thy	Mon Aug 23 11:56:30 2010 +0200
@@ -852,7 +852,7 @@
 lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   by blast
 
-lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
+lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
   -- {* This rewrite rule would confuse users if made default. *}
   by blast
 
@@ -1203,7 +1203,7 @@
 lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
   by (fact inf_eq_top_iff)
 
-lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
   by (fact le_inf_iff)
 
 lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1294,7 +1294,7 @@
 lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
   by (fact sup_eq_bot_iff)
 
-lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
   by (fact le_sup_iff)
 
 lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1490,7 +1490,7 @@
 lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
   by blast
 
-lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
+lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
   by blast
 
 lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"