src/HOL/Multivariate_Analysis/Uniform_Limit.thy

--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Tue Feb 23 18:04:31 2016 +0100
@@ -512,6 +512,7 @@
   unfolding uniformly_convergent_on_def
   by (blast dest: bounded_linear_uniform_limit_intros(13))
 
+
 subsection\<open>Power series and uniform convergence\<close>
 
 proposition powser_uniformly_convergent:
@@ -554,4 +555,5 @@
 apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
 using sm sums_unique by fastforce
 
-end
\ No newline at end of file
+end
+