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.
fix proof broken by changes in dvd theory
authorhuffman
Fri, 09 Jan 2009 09:34:49 -0800
changeset 29412 4085a531153d
parent 29411 85bc8b63747c
child 29413 43a12fc76f48
fix proof broken by changes in dvd theory
src/HOL/NumberTheory/IntPrimes.thy file | annotate | diff | comparison | revisions 
--- 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