src/HOL/Decision_Procs/Polynomial_List.thy
changeset 35028 108662d50512
parent 33268 02de0317f66f
child 36350 bc7982c54e37
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -772,7 +772,7 @@
     1.4  
     1.5  text{*bound for polynomial.*}
     1.6  
     1.7 -lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{ordered_idom})) \<le> poly (map abs p) k"
     1.8 +lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{linordered_idom})) \<le> poly (map abs p) k"
     1.9  apply (induct "p", auto)
    1.10  apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
    1.11  apply (rule abs_triangle_ineq)