src/HOL/Number_Theory/Residues.thy
changeset 66817 0b12755ccbb2
parent 66453 cc19f7ca2ed6
child 66837 6ba663ff2b1c
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -365,8 +365,7 @@
     1.4      done
     1.5    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
     1.6    then show ?thesis
     1.7 -    by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
     1.8 -        cong_int_def res_neg_eq res_one_eq)
     1.9 +    by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int)
    1.10  qed
    1.11  
    1.12  lemma wilson_theorem: