src/HOL/Set.thy
 changeset 39302 d7728f65b353 parent 39213 297cd703f1f0 child 39910 10097e0a9dbd
```     1.1 --- a/src/HOL/Set.thy	Mon Sep 13 08:43:48 2010 +0200
1.2 +++ b/src/HOL/Set.thy	Mon Sep 13 11:13:15 2010 +0200
1.3 @@ -489,20 +489,18 @@
1.4
1.5  subsubsection {* Equality *}
1.6
1.7 -lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
1.8 +lemma set_eqI: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
1.9    apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
1.10     apply (rule Collect_mem_eq)
1.11    apply (rule Collect_mem_eq)
1.12    done
1.13
1.14 -lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
1.15 -by(auto intro:set_ext)
1.16 -
1.17 -lemmas expand_set_eq [no_atp] = set_ext_iff
1.18 +lemma set_eq_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
1.19 +by(auto intro:set_eqI)
1.20
1.21  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
1.22    -- {* Anti-symmetry of the subset relation. *}
1.23 -  by (iprover intro: set_ext subsetD)
1.24 +  by (iprover intro: set_eqI subsetD)
1.25
1.26  text {*
1.27    \medskip Equality rules from ZF set theory -- are they appropriate
```