author blanchet Fri Apr 04 14:44:51 2014 +0200 (2014-04-04) changeset 56403 ae4f904c98b0 parent 56402 6d9a24f87460 child 56404 9cb137ec6ec8
tuned spaces
```     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 04 13:22:26 2014 +0200
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 04 14:44:51 2014 +0200
1.3 @@ -516,10 +516,10 @@
1.4      {fix z::'a
1.5        assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
1.6        from c0 have "norm c > 0" by simp
1.7 -      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z*c)"
1.8 +      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
1.9          by (simp add: field_simps norm_mult)
1.10        have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
1.11 -      from norm_diff_ineq[of "z*c" a ]
1.12 +      from norm_diff_ineq[of "z * c" a ]
1.13        have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
1.15        from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
1.16 @@ -720,7 +720,7 @@
1.17        with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
1.18        have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
1.19        have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
1.20 -      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
1.21 +      have "t * cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
1.22        then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
1.23        from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
1.24          by (simp add: inverse_eq_divide field_simps)
1.25 @@ -1074,4 +1074,3 @@
1.26    shows "poly [:c:] x = y \<longleftrightarrow> c = y" by simp
1.27
1.28  end
1.29 -
```