src/HOL/Number_Theory/Gauss.thy
changeset 62429 25271ff79171
parent 62348 9a5f43dac883
child 63534 523b488b15c9
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Feb 26 18:33:01 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Fri Feb 26 22:15:09 2016 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4    by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
     1.5  
     1.6  lemma A_prod_relprime: "gcd (setprod id A) p = 1"
     1.7 -  by (metis id_def all_A_relprime setprod_coprime_int)
     1.8 +  by (metis id_def all_A_relprime setprod_coprime)
     1.9  
    1.10  
    1.11  subsection \<open>Relationships Between Gauss Sets\<close>