# HG changeset patch
# User wenzelm
# Date 1673809222 -3600
# Node ID 7f7d5c93e36bc47fbd81875d088224c30bb0bc57
# Parent  4c275405faae4bb504f0ea84654de7cd6b08dabe
proper theory context for formal citations;

diff -r 4c275405faae -r 7f7d5c93e36b src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Sun Jan 15 18:30:18 2023 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Sun Jan 15 20:00:22 2023 +0100
@@ -9,6 +9,13 @@
 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,
@@ -22,12 +29,6 @@
 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>