--- 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 *)