Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Number_Theory/Residues.thy
changeset 66954 0230af0f3c59
parent 66888 930abfdf8727
child 67051 e7e54a0b9197 
--- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -291,8 +291,8 @@
 next
   case False
   with assms show ?thesis
-    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
-    by (auto simp add: residues_def gcd_int_def) force
+    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
+    by (auto simp add: residues_def gcd_int_def) fastforce
 qed
 
 lemma fermat_theorem:
isabelle