# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391691846 0
# Node ID d344d663658a2a50f204175eda7b796a34a85447
# Parent  8a53ee72e595c82527d18f6e6c5c6717a68aba17
fixed problem (?) by deleting "thm" line

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 "