Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid internal fact
authorblanchet
Tue, 09 Sep 2014 22:28:49 +0200
changeset 58288 87b59745dd6d
parent 58287 10105897bc22
child 58289 eb93bc67d361
avoid internal fact
src/HOL/Number_Theory/Gauss.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Number_Theory/Gauss.thy	Tue Sep 09 22:25:14 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Tue Sep 09 22:28:49 2014 +0200
@@ -206,7 +206,7 @@
   by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
 
 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
-  by (metis DEADID.map_id all_A_relprime setprod_coprime_int)
+  by (metis id_def all_A_relprime setprod_coprime_int)
 
 
 subsection {* Relationships Between Gauss Sets *}
isabelle