
diff -r 9096703ed99e -r ff203584b36e src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Tue Jan 17 15:55:52 2023 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Tue Jan 17 16:08:54 2023 +0100
@@ -9,13 +9,6 @@
 section \<open>Infinite sums\<close>
 \<^latex>\<open>\label{section:Infinite_Sum}\<close>
 
-theory Infinite_Sum
-  imports
-    Elementary_Topology
-    "HOL-Library.Extended_Nonnegative_Real"
-    "HOL-Library.Complex_Order"
-begin
-
 text \<open>In this theory, we introduce the definition of infinite sums, i.e., sums ranging over an
 infinite, potentially uncountable index set with no particular ordering.
 (This is different from series. Those are sums indexed by natural numbers,
@@ -29,6 +22,12 @@
 commutative monoid endowed with a Hausdorff topology.
 (Examples are reals, complex numbers, normed vector spaces, and more.)\<close>
 
+theory Infinite_Sum
+  imports
+    Elementary_Topology
+    "HOL-Library.Extended_Nonnegative_Real"
+    "HOL-Library.Complex_Order"
+begin
 
 subsection \<open>Definition and syntax\<close>
 




