src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 56544 b60d5d119489
parent 56403 ae4f904c98b0
child 56776 309e1a61ee7c
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -361,7 +361,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 mult_pos_pos)
     1.8 +      by (simp_all add: field_simps)
     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