src/HOL/Set.thy
changeset 15554 03d4347b071d
parent 15535 a0cf3a19ee36
child 15950 5c067c956a20
     1.1 --- a/src/HOL/Set.thy	Tue Mar 01 05:44:13 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Mar 01 18:48:52 2005 +0100
     1.3 @@ -520,6 +520,10 @@
     1.4    apply (rule Collect_mem_eq)
     1.5    done
     1.6  
     1.7 +(* Due to Brian Huffman *)
     1.8 +lemma expand_set_eq: "(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"
    1.12    -- {* Anti-symmetry of the subset relation. *}
    1.13    by (rules intro: set_ext subsetD)