src/HOL/Old_Number_Theory/WilsonRuss.thy

--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sun Apr 01 23:21:54 2012 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Apr 02 09:18:16 2012 +0200
@@ -60,11 +60,6 @@
   apply safe
   apply (cut_tac a = a and p = p in inv_is_inv)
      apply (unfold zcong_def, auto)
-  apply (subgoal_tac "\<not> p dvd 1")
-   apply (rule_tac [2] zdvd_not_zless)
-    apply (subgoal_tac "p dvd 1")
-     prefer 2
-     apply (subst dvd_minus_iff [symmetric], auto)
   done
 
 lemma inv_not_1: