# HG changeset patch
# User wenzelm
# Date 1673968134 -3600
# Node ID ff203584b36ee879d21b831548c2047bed63a757
# Parent  9096703ed99edcfc7eed75b43cca2faabbb1b4ce
backed out changeset 7f7d5c93e36b: no longer required thanks to 9096703ed99e;

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>