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 29412 4085a531153d
parent 27651 16a26996c30e
child 29667 53103fc8ffa3 
--- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Jan 08 21:13:40 2009 -0800
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Fri Jan 09 09:34:49 2009 -0800
@@ -94,7 +94,7 @@
 
 lemma zgcd_zdvd_zgcd_zmult: "zgcd m n dvd zgcd (k * m) n"
   apply (simp add: zgcd_greatest_iff)
-  apply (blast intro: zdvd_trans)
+  apply (blast intro: zdvd_trans dvd_triv_right)
   done
 
 lemma zgcd_zmult_zdvd_zgcd:
isabelle