src/HOL/Library/Polynomial.thy
changeset 31021 53642251a04f
parent 30960 fec1a04b7220
child 31663 5eb82f064630
--- a/src/HOL/Library/Polynomial.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -632,8 +632,6 @@
   shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
   by (safe elim!: dvd_smult dvd_smult_cancel)
 
-instance poly :: (comm_semiring_1) recpower ..
-
 lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
 by (induct n, simp, auto intro: order_trans degree_mult_le)
 
@@ -1120,7 +1118,7 @@
   unfolding one_poly_def by simp
 
 lemma poly_monom:
-  fixes a x :: "'a::{comm_semiring_1,recpower}"
+  fixes a x :: "'a::{comm_semiring_1}"
   shows "poly (monom a n) x = a * x ^ n"
   by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
 
@@ -1149,7 +1147,7 @@
   by (induct p, simp_all, simp add: algebra_simps)
 
 lemma poly_power [simp]:
-  fixes p :: "'a::{comm_semiring_1,recpower} poly"
+  fixes p :: "'a::{comm_semiring_1} poly"
   shows "poly (p ^ n) x = poly p x ^ n"
   by (induct n, simp, simp add: power_Suc)