# HG changeset patch
# User blanchet
# Date 1282558438 -7200
# Node ID 14c207135effab872bc10badce8bfc2c9a5e6758
# Parent  52ea97d95e4bed5194a156571377b50b576e0143
"no_atp" fact that leads to unsound proofs

diff -r 52ea97d95e4b -r 14c207135eff src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Aug 23 11:56:30 2010 +0200
+++ b/src/HOL/Set.thy	Mon Aug 23 12:13:58 2010 +0200
@@ -495,7 +495,7 @@
   apply (rule Collect_mem_eq)
   done
 
-lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
+lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
 by(auto intro:set_ext)
 
 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"