src/HOL/Library/Polynomial.thy
changeset 35028 108662d50512
parent 34973 ae634fad947e
child 36350 bc7982c54e37
     1.1 --- a/src/HOL/Library/Polynomial.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -706,7 +706,7 @@
     1.4  subsection {* Polynomials form an ordered integral domain *}
     1.5  
     1.6  definition
     1.7 -  pos_poly :: "'a::ordered_idom poly \<Rightarrow> bool"
     1.8 +  pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
     1.9  where
    1.10    "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
    1.11  
    1.12 @@ -732,7 +732,7 @@
    1.13  lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
    1.14  by (induct p) (auto simp add: pos_poly_pCons)
    1.15  
    1.16 -instantiation poly :: (ordered_idom) ordered_idom
    1.17 +instantiation poly :: (linordered_idom) linordered_idom
    1.18  begin
    1.19  
    1.20  definition