diff -r 70d4d9e5707b -r f8652d0534fa src/HOL/Quotient_Examples/Int_Pow.thy
--- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jul 22 11:00:43 2016 +0200
@@ -41,8 +41,8 @@
   "[| x \<in> Units G; y \<in> Units G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
 proof -
   assume G: "x \<in> Units G"  "y \<in> Units G"
-  moreover then have "x \<in> carrier G"  "y \<in> carrier G" by auto
-  ultimately have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
+  then have "x \<in> carrier G"  "y \<in> carrier G" by auto
+  with G have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
     by (simp add: m_assoc) (simp add: m_assoc [symmetric])
   with G show ?thesis by (simp del: Units_l_inv)
 qed