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/NumberTheory/IntPrimes.thy
changeset 29948 cdf12a1cb963
parent 29925 17d1e32ef867
child 30034 60f64f112174
child 30240 5b25fee0362c 
--- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Feb 17 18:48:17 2009 +0100
@@ -88,7 +88,7 @@
 
 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
   apply (rule zgcd_eq [THEN trans])
-  apply (simp add: zmod_zadd1_eq)
+  apply (simp add: mod_add_eq)
   apply (rule zgcd_eq [symmetric])
   done
isabelle