src/HOL/Library/Polynomial.thy

 
 
 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)"
 
 lemma pos_poly_pCons:
   "pos_poly (pCons a p) \<longleftrightarrow> pos_poly p \<or> (p = 0 \<and> 0 < a)"

   done
 
 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
   [code del]:
     "x < y \<longleftrightarrow> pos_poly (y - x)"