src/HOL/Equiv_Relations.thy
changeset 18493 343da052b961
parent 18490 434e34392c40
child 19323 ec5cd5b1804c
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Dec 22 14:22:11 2005 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Dec 22 17:57:09 2005 +0100
     1.3 @@ -90,10 +90,6 @@
     1.4    "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
     1.5    by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
     1.6  
     1.7 -lemma eq_equiv_class_iff2:
     1.8 -  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
     1.9 -by(simp add:quotient_def eq_equiv_class_iff)
    1.10 -
    1.11  
    1.12  subsection {* Quotients *}
    1.13  
    1.14 @@ -136,6 +132,10 @@
    1.15    apply (unfold equiv_def sym_def trans_def, blast)
    1.16    done
    1.17  
    1.18 +lemma eq_equiv_class_iff2:
    1.19 +  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
    1.20 +by(simp add:quotient_def eq_equiv_class_iff)
    1.21 +
    1.22  
    1.23  lemma quotient_empty [simp]: "{}//r = {}"
    1.24  by(simp add: quotient_def)