--- 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
--- 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"
--- 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.