src/HOL/Analysis/Analysis.thy

--- a/src/HOL/Analysis/Analysis.thy	Wed May 03 10:35:20 2023 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Wed May 03 11:20:03 2023 +0100
@@ -4,6 +4,8 @@
   Convex
   Determinants
   (* Topology *)
+  FSigma
+  Sum_Topology
   Connected
   Abstract_Limits
   Isolated