# HG changeset patch
# User huffman
# Date 1231522489 28800
# Node ID 4085a531153da78bb81ae95e9101875ceaf39e28
# Parent  85bc8b63747c24f74f32d72139c5718ff62b5e3d
fix proof broken by changes in dvd theory

diff -r 85bc8b63747c -r 4085a531153d src/HOL/NumberTheory/IntPrimes.thy
--- 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: