src/HOL/Library/Polynomial.thy
changeset 59557 ebd8ecacfba6
parent 59487 adaa430fc0f7
child 59815 cce82e360c2f
     1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Feb 18 22:46:48 2015 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Feb 19 11:53:36 2015 +0100
     1.3 @@ -710,7 +710,7 @@
     1.4  lemma [code]:
     1.5    fixes p q :: "'a::ab_group_add poly"
     1.6    shows "p - q = p + - q"
     1.7 -  by (fact ab_add_uminus_conv_diff)
     1.8 +  by (fact diff_conv_add_uminus)
     1.9  
    1.10  lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
    1.11    apply (induct p arbitrary: q, simp)
    1.12 @@ -1518,7 +1518,7 @@
    1.13    assumes "pdivmod_rel x' y q' r'"
    1.14    shows "pdivmod_rel (x + x') y (q + q') (r + r')"
    1.15    using assms unfolding pdivmod_rel_def
    1.16 -  by (auto simp add: distrib degree_add_less)
    1.17 +  by (auto simp add: algebra_simps degree_add_less)
    1.18  
    1.19  lemma poly_div_add_left:
    1.20    fixes x y z :: "'a::field poly"