src/HOL/Library/Polynomial.thy
changeset 31021 53642251a04f
parent 30960 fec1a04b7220
child 31663 5eb82f064630
     1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Apr 28 19:15:50 2009 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Apr 29 14:20:26 2009 +0200
     1.3 @@ -632,8 +632,6 @@
     1.4    shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
     1.5    by (safe elim!: dvd_smult dvd_smult_cancel)
     1.6  
     1.7 -instance poly :: (comm_semiring_1) recpower ..
     1.8 -
     1.9  lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
    1.10  by (induct n, simp, auto intro: order_trans degree_mult_le)
    1.11  
    1.12 @@ -1120,7 +1118,7 @@
    1.13    unfolding one_poly_def by simp
    1.14  
    1.15  lemma poly_monom:
    1.16 -  fixes a x :: "'a::{comm_semiring_1,recpower}"
    1.17 +  fixes a x :: "'a::{comm_semiring_1}"
    1.18    shows "poly (monom a n) x = a * x ^ n"
    1.19    by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
    1.20  
    1.21 @@ -1149,7 +1147,7 @@
    1.22    by (induct p, simp_all, simp add: algebra_simps)
    1.23  
    1.24  lemma poly_power [simp]:
    1.25 -  fixes p :: "'a::{comm_semiring_1,recpower} poly"
    1.26 +  fixes p :: "'a::{comm_semiring_1} poly"
    1.27    shows "poly (p ^ n) x = poly p x ^ n"
    1.28    by (induct n, simp, simp add: power_Suc)
    1.29