src/HOL/Equiv_Relations.thy
changeset 44204 3cdc4176638c
parent 40945 b8703f63bfb2
child 44278 1220ecb81e8f
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Aug 15 22:31:17 2011 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Tue Aug 16 07:17:15 2011 +0900
     1.3 @@ -402,8 +402,8 @@
     1.4    by (erule part_equivpE, erule transpE)
     1.5  
     1.6  lemma part_equivp_typedef:
     1.7 -  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
     1.8 -  by (auto elim: part_equivpE simp add: mem_def)
     1.9 +  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}"
    1.10 +  by (auto elim: part_equivpE)
    1.11  
    1.12  
    1.13  text {* Total equivalences *}