--- a/src/HOL/Library/Formal_Power_Series.thy Sat Feb 14 11:11:30 2009 -0800
+++ b/src/HOL/Library/Formal_Power_Series.thy Sat Feb 14 11:32:35 2009 -0800
@@ -496,7 +496,7 @@
by(simp add: setsum_delta)
qed
-subsection{* Formal Derivatives, and the McLaurin theorem around 0*}
+subsection{* Formal Derivatives, and the MacLaurin theorem around 0*}
definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
@@ -695,7 +695,7 @@
ultimately show ?thesis by blast
qed
-lemma fps_sqrare_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2 \<longleftrightarrow> (a = b \<or> a = -b)"
+lemma fps_square_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2 \<longleftrightarrow> (a = b \<or> a = -b)"
proof-
{assume "a = b \<or> a = -b" hence "a^2 = b^2" by auto}
moreover