1.1 --- a/src/HOL/Set.thy	Tue Sep 07 15:56:33 2010 -0700
     1.2 +++ b/src/HOL/Set.thy	Wed Sep 08 10:45:55 2010 +0200
     1.3 @@ -498,6 +498,8 @@
     1.4  lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
     1.5  by(auto intro:set_ext)
     1.6  
     1.7 +lemmas expand_set_eq [no_atp] = set_ext_iff
     1.8 +
     1.9  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    1.10    -- {* Anti-symmetry of the subset relation. *}
    1.11    by (iprover intro: set_ext subsetD)