diff -r 0b91269c0b13 -r 449a70d88b38 src/ZF/Integ/EquivClass.thy
--- a/src/ZF/Integ/EquivClass.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Integ/EquivClass.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -149,18 +149,15 @@
      ==> X=Y"
 apply (unfold quotient_def, safe)
 apply (rule equiv_class_eq, assumption)
-apply (rotate_tac -2) 
 apply (simp add: UN_equiv_class [of A r b])  
 done
 
 
 subsection{*Defining Binary Operations upon Equivalence Classes*}
 
-
 lemma congruent2_implies_congruent:
     "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))"
-apply (unfold congruent_def congruent2_def equiv_def refl_def, blast)
-done
+by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
 
 lemma congruent2_implies_congruent_UN:
     "[| equiv(A,r);  congruent2(r,b);  a: A |] ==>