| changeset 39198 | f967a16dfcdd |
| parent 38864 | 4abe644fcea5 |
| child 39213 | 297cd703f1f0 |
--- a/src/HOL/Set.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Set.thy Tue Sep 07 10:05:19 2010 +0200 @@ -495,7 +495,7 @@ apply (rule Collect_mem_eq) done -lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))" +lemma set_ext_iff [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"