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