1.1 --- a/src/ZF/EquivClass.thy	Tue Mar 06 15:15:49 2012 +0000
     1.2 +++ b/src/ZF/EquivClass.thy	Tue Mar 06 16:06:52 2012 +0000
     1.3 @@ -92,11 +92,11 @@
     1.4  by (unfold equiv_def, blast)
     1.5  
     1.6  lemma equiv_class_eq_iff:
     1.7 -     "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
     1.8 +     "equiv(A,r) ==> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x:A & y:A"
     1.9  by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    1.10  
    1.11  lemma eq_equiv_class_iff:
    1.12 -     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
    1.13 +     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"
    1.14  by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    1.15  
    1.16  (*** Quotients ***)