diff -r f3d19c8445ec -r 24b70433c2e8 src/HOL/Analysis/Analysis.thy --- a/src/HOL/Analysis/Analysis.thy Tue May 30 12:07:48 2023 +0200 +++ b/src/HOL/Analysis/Analysis.thy Tue May 30 12:33:06 2023 +0100 @@ -8,6 +8,7 @@ Sum_Topology Abstract_Topological_Spaces Abstract_Metric_Spaces + Urysohn Connected Abstract_Limits Isolated