# HG changeset patch
# User wenzelm
# Date 1203958183 -3600
# Node ID 01f4e5d21eaf177aeab58068f9bbf09d31579e6f
# Parent  3b499feded50fa7f0e333a71cd7768df0e10c95e
fixed document;

diff -r 3b499feded50 -r 01f4e5d21eaf src/HOL/Complex/Fundamental_Theorem_Algebra.thy
--- 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"