src/HOL/Series.thy
changeset 61799 4cf66f21b764
parent 61609 77b453bd616f
child 61969 e01015e49041
     1.1 --- a/src/HOL/Series.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Series.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -384,7 +384,7 @@
     1.4  lemma summable_minus_iff:
     1.5    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
     1.6    shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
     1.7 -  by (auto dest: summable_minus) --\<open>used two ways, hence must be outside the context above\<close>
     1.8 +  by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
     1.9  
    1.10  
    1.11  context