src/HOL/Series.thy
changeset 63145 703edebd1d92
parent 63040 eb4ddd18d635
child 63365 5340fb6633d0
     1.1 --- a/src/HOL/Series.thy	Tue May 24 22:46:23 2016 +0200
     1.2 +++ b/src/HOL/Series.thy	Wed May 25 11:49:40 2016 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -context --\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
     1.8 +context \<comment>\<open>Separate contexts are necessary to allow general use of the results above, here.\<close>
     1.9    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.10  begin
    1.11