src/HOL/Set.thy

--- a/src/HOL/Set.thy	Tue Mar 01 05:44:13 2005 +0100
+++ b/src/HOL/Set.thy	Tue Mar 01 18:48:52 2005 +0100
@@ -520,6 +520,10 @@
   apply (rule Collect_mem_eq)
   done
 
+(* Due to Brian Huffman *)
+lemma expand_set_eq: "(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"
   -- {* Anti-symmetry of the subset relation. *}
   by (rules intro: set_ext subsetD)