src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 36778 739a9379e29b
parent 34915 7894c7dab132
child 36975 fa6244be5215
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun May 09 17:47:43 2010 -0700
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun May 09 22:51:11 2010 -0700
     1.3 @@ -355,7 +355,7 @@
     1.4      from real_lbound_gt_zero[OF one0 em0]
     1.5      obtain d where d: "d >0" "d < 1" "d < e / m" by blast
     1.6      from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
     1.7 -      by (simp_all add: field_simps real_mult_order)
     1.8 +      by (simp_all add: field_simps mult_pos_pos)
     1.9      show ?case
    1.10        proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
    1.11          fix d w