avoid internal fact
authorblanchet
Tue Sep 09 22:28:49 2014 +0200 (2014-09-09)
changeset 5828887b59745dd6d
parent 58287 10105897bc22
child 58289 eb93bc67d361
avoid internal fact
src/HOL/Number_Theory/Gauss.thy
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Tue Sep 09 22:25:14 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Tue Sep 09 22:28:49 2014 +0200
     1.3 @@ -206,7 +206,7 @@
     1.4    by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
     1.5  
     1.6  lemma A_prod_relprime: "gcd (setprod id A) p = 1"
     1.7 -  by (metis DEADID.map_id all_A_relprime setprod_coprime_int)
     1.8 +  by (metis id_def all_A_relprime setprod_coprime_int)
     1.9  
    1.10  
    1.11  subsection {* Relationships Between Gauss Sets *}