# HG changeset patch
# User immler
# Date 1575313662 18000
# Node ID 0aaf16a0f7cce99580c918f7a1988fe1940fe473
# Parent  1bf7d1acbe74298b809af2cae4e108cdc5e9dfa0# Parent  29e7c6d11cf1b8dd4b25abbe1b31970a5e1744e7
merged

diff -r 29e7c6d11cf1 -r 0aaf16a0f7cc src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Mon Dec 02 17:15:17 2019 +0000
+++ b/src/HOL/Analysis/Analysis.thy	Mon Dec 02 14:07:42 2019 -0500
@@ -6,7 +6,6 @@
   (* Topology *)
   Connected
   Abstract_Limits
-  Abstract_Euclidean_Space
   (* Functional Analysis *)
   Elementary_Normed_Spaces
   Norm_Arith
@@ -46,6 +45,7 @@
   Simplex_Content
   FPS_Convergence
   Smooth_Paths
+  Abstract_Euclidean_Space
 begin
 
 end
diff -r 29e7c6d11cf1 -r 0aaf16a0f7cc src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Dec 02 17:15:17 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Mon Dec 02 14:07:42 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"
diff -r 29e7c6d11cf1 -r 0aaf16a0f7cc src/HOL/Analysis/Metric_Arith.thy
--- a/src/HOL/Analysis/Metric_Arith.thy	Mon Dec 02 17:15:17 2019 +0000
+++ b/src/HOL/Analysis/Metric_Arith.thy	Mon Dec 02 14:07:42 2019 -0500
@@ -2,13 +2,15 @@
     Author:   Maximilian Schäffeler (port from HOL Light)
 *)
 
-section \<open>A decision procedure for metric spaces\<close>
+chapter \<open>Functional Analysis\<close>
+
+section\<^marker>\<open>tag unimportant\<close> \<open>A decision procedure for metric spaces\<close>
 
 theory Metric_Arith
   imports HOL.Real_Vector_Spaces
 begin
 
-text \<open>
+text\<^marker>\<open>tag unimportant\<close> \<open>
 A port of the decision procedure ``Formalization of metric spaces in HOL Light''
 @{cite "DBLP:journals/jar/Maggesi18"} for the type class @{class metric_space},
 with the \<open>Argo\<close> solver as backend.