| changeset 38649 | 14c207135eff |
| parent 38648 | 52ea97d95e4b |
| child 38715 | 6513ea67d95d |
--- 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"