author | blanchet |
Mon, 23 Aug 2010 12:13:58 +0200 | |
changeset 38887 | 14c207135eff |
parent 38886 | 52ea97d95e4b |
child 38888 | f22a564ac820 |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
1.1 --- a/src/HOL/Set.thy Mon Aug 23 11:56:30 2010 +0200 1.2 +++ b/src/HOL/Set.thy Mon Aug 23 12:13:58 2010 +0200 1.3 @@ -495,7 +495,7 @@ 1.4 apply (rule Collect_mem_eq) 1.5 done 1.6 1.7 -lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))" 1.8 +lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))" 1.9 by(auto intro:set_ext) 1.10 1.11 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"