src/HOL/Equiv_Relations.thy
changeset 18490 434e34392c40
parent 17589 58eeffd73be1
child 18493 343da052b961
     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Dec 22 12:27:10 2005 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Dec 22 13:00:53 2005 +0100
     1.3 @@ -90,6 +90,10 @@
     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