--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Mon Feb 25 17:27:41 2008 +0100
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Mon Feb 25 17:49:43 2008 +0100
@@ -134,7 +134,7 @@
text{* Offsetting the variable in a polynomial gives another of same degree *}
- (* FIXME : Lemma holds also in locale --- fix it laster *)
+ (* FIXME : Lemma holds also in locale --- fix it later *)
lemma poly_offset_lemma:
shows "\<exists>b q. (length q = length p) \<and> (\<forall>x. poly (b#q) (x::complex) = (a + x) * poly p x)"
proof(induct p)
@@ -379,7 +379,7 @@
thus ?thesis unfolding linorder_not_le[symmetric] by blast
qed
-text{* Hence we can always reduce modulus of 1 + b z^n if nonzero *}
+text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
lemma reduce_poly_simple:
assumes b: "b \<noteq> 0" and n: "n\<noteq>0"
shows "\<exists>z. cmod (1 + b * z^n) < 1"