src/HOL/Library/Polynomial.thy
changeset 57512 cc97b347b301
parent 57482 60459c3853af
child 57862 8f074e6e22fc
     1.1 --- a/src/HOL/Library/Polynomial.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -624,9 +624,9 @@
     1.4  instance proof
     1.5    fix p q r :: "'a poly"
     1.6    show "(p + q) + r = p + (q + r)"
     1.7 -    by (simp add: poly_eq_iff add_assoc)
     1.8 +    by (simp add: poly_eq_iff add.assoc)
     1.9    show "p + q = q + p"
    1.10 -    by (simp add: poly_eq_iff add_commute)
    1.11 +    by (simp add: poly_eq_iff add.commute)
    1.12    show "0 + p = p"
    1.13      by (simp add: poly_eq_iff)
    1.14  qed
    1.15 @@ -713,7 +713,7 @@
    1.16  lemma degree_add_eq_left:
    1.17    "degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
    1.18    using degree_add_eq_right [of q p]
    1.19 -  by (simp add: add_commute)
    1.20 +  by (simp add: add.commute)
    1.21  
    1.22  lemma degree_minus [simp]: "degree (- p) = degree p"
    1.23    unfolding degree_def by simp
    1.24 @@ -824,7 +824,7 @@
    1.25    by (rule degree_le, simp add: coeff_eq_0)
    1.26  
    1.27  lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
    1.28 -  by (rule poly_eqI, simp add: mult_assoc)
    1.29 +  by (rule poly_eqI, simp add: mult.assoc)
    1.30  
    1.31  lemma smult_0_right [simp]: "smult a 0 = 0"
    1.32    by (rule poly_eqI, simp)