
diff -r 8a53ee72e595 -r d344d663658a src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Thu Feb 06 01:13:44 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Feb 06 13:04:06 2014 +0000
@@ -655,8 +655,9 @@
       have False
         by simp}
     then have b0: "b \<noteq> 0" ..
-    hence b1: "b \<ge> 1" by arith thm Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1]]
-    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] ath b1 b(2) nqr
+    hence b1: "b \<ge> 1" by arith 
+    from cong_imp_coprime_nat[OF Cong.cong_diff_nat[OF cong_sym_nat [OF b(1)] cong_refl_nat[of 1] b1]] 
+         ath b1 b nqr
     have "coprime (a ^ ((n - 1) div p) - 1) n"
       by simp}
   hence th: "\<forall>p. prime p \<and> p dvd q \<longrightarrow> coprime (a ^ ((n - 1) div p) - 1) n "




