src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 47268 262d96552e50
parent 47164 6a4c479ba94f
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sun Apr 01 23:21:54 2012 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Apr 02 09:18:16 2012 +0200
     1.3 @@ -60,11 +60,6 @@
     1.4    apply safe
     1.5    apply (cut_tac a = a and p = p in inv_is_inv)
     1.6       apply (unfold zcong_def, auto)
     1.7 -  apply (subgoal_tac "\<not> p dvd 1")
     1.8 -   apply (rule_tac [2] zdvd_not_zless)
     1.9 -    apply (subgoal_tac "p dvd 1")
    1.10 -     prefer 2
    1.11 -     apply (subst dvd_minus_iff [symmetric], auto)
    1.12    done
    1.13  
    1.14  lemma inv_not_1: