diff -r 36961c681fed -r 1bf7d1acbe74 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Dec 02 13:41:44 2019 -0500
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Dec 02 13:57:32 2019 -0500
@@ -4,7 +4,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-chapter \<open>Functional Analysis\<close>
+section \<open>Elementary Metric Spaces\<close>
 
 theory Elementary_Metric_Spaces
   imports
@@ -12,8 +12,6 @@
     Metric_Arith
 begin
 
-section \<open>Elementary Metric Spaces\<close>
-
 subsection \<open>Open and closed balls\<close>
 
 definition\<^marker>\<open>tag important\<close> ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"