src/HOL/Library/Formal_Power_Series.thy

     apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
     unfolding th2
     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))"
 
 lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)" by (simp add: fps_deriv_def)
 

   {assume "a + b = 0" hence "a + b - b = -b" by simp
     hence "a = -b" by simp}
   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
   {assume "a^2 = b^2 "
     hence "a^2 - b^2 = 0" by simp