--- a/src/HOL/Library/Polynomial.thy Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Library/Polynomial.thy Fri Feb 05 14:33:50 2010 +0100
@@ -706,7 +706,7 @@
subsection {* Polynomials form an ordered integral domain *}
definition
- pos_poly :: "'a::ordered_idom poly \<Rightarrow> bool"
+ pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
where
"pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
@@ -732,7 +732,7 @@
lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
by (induct p) (auto simp add: pos_poly_pCons)
-instantiation poly :: (ordered_idom) ordered_idom
+instantiation poly :: (linordered_idom) linordered_idom
begin
definition