src/HOL/Library/Polynomial.thy
changeset 44890 22f665a2e91c
parent 41959 b460124855b8
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/Library/Polynomial.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -1134,7 +1134,7 @@
     1.4    and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
     1.5    apply (induct x y rule: poly_gcd.induct)
     1.6    apply (simp_all add: poly_gcd.simps)
     1.7 -  apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
     1.8 +  apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
     1.9    apply (blast dest: dvd_mod_imp_dvd)
    1.10    done
    1.11