diff -r cff7114e4572 -r 755fda743c49 src/HOL/Multivariate_Analysis/Summation.thy
--- a/src/HOL/Multivariate_Analysis/Summation.thy	Mon Jan 04 22:13:53 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Summation.thy	Tue Jan 05 13:35:06 2016 +0100
@@ -1,10 +1,9 @@
-(*
-  Title:    HOL/Multivariate_Analysis/Summation.thy
-  Author:   Manuel Eberl, TU München
+(*  Title:    HOL/Multivariate_Analysis/Summation.thy
+    Author:   Manuel Eberl, TU München
+*)
   
-  The definition of the radius of convergence of a power series, 
-  various summability tests, lemmas to compute the radius of convergence etc.
-*)
+section \<open>Rounded dual logarithm\<close>
+
 theory Summation
 imports
   Complex_Main
@@ -12,7 +11,10 @@
   "~~/src/HOL/Library/Liminf_Limsup"
 begin
 
-subsection \<open>Rounded dual logarithm\<close>
+text \<open>
+  The definition of the radius of convergence of a power series, 
+  various summability tests, lemmas to compute the radius of convergence etc.
+\<close>
 
 (* This is required for the Cauchy condensation criterion *)