--- a/src/HOL/Equiv_Relations.thy Thu Dec 22 12:27:10 2005 +0100
+++ b/src/HOL/Equiv_Relations.thy Thu Dec 22 13:00:53 2005 +0100
@@ -90,6 +90,10 @@
"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 *}