src/HOL/Equiv_Relations.thy

--- a/src/HOL/Equiv_Relations.thy	Thu Dec 22 14:22:11 2005 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Dec 22 17:57:09 2005 +0100
@@ -90,10 +90,6 @@
   "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
 
-lemma eq_equiv_class_iff2:
-  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
-by(simp add:quotient_def eq_equiv_class_iff)
-
 
 subsection {* Quotients *}
 
@@ -136,6 +132,10 @@
   apply (unfold equiv_def sym_def trans_def, blast)
   done
 
+lemma eq_equiv_class_iff2:
+  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
+by(simp add:quotient_def eq_equiv_class_iff)
+
 
 lemma quotient_empty [simp]: "{}//r = {}"
 by(simp add: quotient_def)