--- a/src/HOL/Analysis/Connected.thy Fri Nov 15 16:44:09 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy Fri Nov 15 21:09:03 2019 +0100
@@ -569,9 +569,9 @@
qed
+subsection\<open>Lemmas about components\<close>
-subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
-
+text \<open>See Newman IV, 3.3 and 3.4.\<close>
lemma connected_Un_clopen_in_complement:
fixes S U :: "'a::metric_space set"
--- a/src/HOL/Analysis/Locally.thy Fri Nov 15 16:44:09 2019 +0100
+++ b/src/HOL/Analysis/Locally.thy Fri Nov 15 21:09:03 2019 +0100
@@ -1,11 +1,13 @@
-section \<open>Neigbourhood bases and Locally path-connected spaces\<close>
+section \<open>Neighbourhood bases and Locally path-connected spaces\<close>
theory Locally
imports
Path_Connected Function_Topology
begin
-subsection\<open>Neigbourhood bases (useful for "local" properties of various kinds)\<close>
+subsection\<open>Neighbourhood Bases\<close>
+
+text \<open>Useful for "local" properties of various kinds\<close>
definition neighbourhood_base_at where
"neighbourhood_base_at x P X \<equiv>