fix spelling
authorhuffman
Sat Feb 14 11:32:35 2009 -0800 (2009-02-14)
changeset 29912f4ac160d2e77
parent 29911 c790a70a3d19
child 29913 89eadbe71e97
fix spelling
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 11:11:30 2009 -0800
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Feb 14 11:32:35 2009 -0800
     1.3 @@ -496,7 +496,7 @@
     1.4      by(simp add: setsum_delta)
     1.5  qed
     1.6  
     1.7 -subsection{* Formal Derivatives, and the McLaurin theorem around 0*}
     1.8 +subsection{* Formal Derivatives, and the MacLaurin theorem around 0*}
     1.9  
    1.10  definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
    1.11  
    1.12 @@ -695,7 +695,7 @@
    1.13    ultimately show ?thesis by blast
    1.14  qed
    1.15  
    1.16 -lemma fps_sqrare_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2  \<longleftrightarrow> (a = b \<or> a = -b)"
    1.17 +lemma fps_square_eq_iff: "(a:: 'a::idom fps)^ 2 = b^2  \<longleftrightarrow> (a = b \<or> a = -b)"
    1.18  proof-
    1.19    {assume "a = b \<or> a = -b" hence "a^2 = b^2" by auto}
    1.20    moreover