# HG changeset patch
# User huffman
# Date 1234639955 28800
# Node ID f4ac160d2e77f23da4c1013e43371f82e44db8c4
# Parent  c790a70a3d19222d8bf7d587e747c0658e437c35
fix spelling

diff -r c790a70a3d19 -r f4ac160d2e77 src/HOL/Library/Formal_Power_Series.thy
--- 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