src/HOL/Library/Polynomial.thy
changeset 60686 ea5bc46c11e6
parent 60685 cb21b7022b00
child 61260 e6f03fae14d5
     1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jul 08 14:01:34 2015 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Jul 08 14:01:39 2015 +0200
     1.3 @@ -1832,7 +1832,7 @@
     1.4  lemma dvd_poly_gcd_iff [iff]:
     1.5    fixes k x y :: "_ poly"
     1.6    shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
     1.7 -  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
     1.8 +  by (auto intro!: poly_gcd_greatest intro: dvd_trans [of _ "gcd x y"])
     1.9  
    1.10  lemma poly_gcd_monic:
    1.11    fixes x y :: "_ poly"