diff --git a/src/HOL/Analysis/Metric_Arith.thy b/src/HOL/Analysis/Metric_Arith.thy
--- a/src/HOL/Analysis/Metric_Arith.thy
+++ b/src/HOL/Analysis/Metric_Arith.thy
@@ -1,103 +1,109 @@
 (*  Title:    Metric_Arith.thy
     Author:   Maximilian Schäffeler (port from HOL Light)
 *)
 
 section \<open>A decision procedure for metric spaces\<close>
 
 theory Metric_Arith
   imports HOL.Real_Vector_Spaces
 begin
 
+text \<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.
+\<close>
+
 named_theorems metric_prenex
 named_theorems metric_nnf
 named_theorems metric_unfold
 named_theorems metric_pre_arith
 
 lemmas pre_arith_simps =
   max.bounded_iff max_less_iff_conj
   le_max_iff_disj less_max_iff_disj
   simp_thms HOL.eq_commute
 declare pre_arith_simps [metric_pre_arith]
 
 lemmas unfold_simps =
   Un_iff subset_iff disjoint_iff_not_equal
   Ball_def Bex_def
 declare unfold_simps [metric_unfold]
 
 declare HOL.nnf_simps(4) [metric_prenex]
 
 lemma imp_prenex [metric_prenex]:
   "\<And>P Q. (\<exists>x. P x) \<longrightarrow> Q \<equiv> \<forall>x. (P x \<longrightarrow> Q)"
   "\<And>P Q. P \<longrightarrow> (\<exists>x. Q x) \<equiv> \<exists>x. (P \<longrightarrow> Q x)"
   "\<And>P Q. (\<forall>x. P x) \<longrightarrow> Q \<equiv> \<exists>x. (P x \<longrightarrow> Q)"
   "\<And>P Q. P \<longrightarrow> (\<forall>x. Q x) \<equiv> \<forall>x. (P \<longrightarrow> Q x)"
   by simp_all
 
 lemma ex_prenex [metric_prenex]:
   "\<And>P Q. (\<exists>x. P x) \<and> Q \<equiv> \<exists>x. (P x \<and> Q)"
   "\<And>P Q. P \<and> (\<exists>x. Q x) \<equiv> \<exists>x. (P \<and> Q x)"
   "\<And>P Q. (\<exists>x. P x) \<or> Q \<equiv> \<exists>x. (P x \<or> Q)"
   "\<And>P Q. P \<or> (\<exists>x. Q x) \<equiv> \<exists>x. (P \<or> Q x)"
   "\<And>P. \<not>(\<exists>x. P x) \<equiv> \<forall>x. \<not>P x"
   by simp_all
 
 lemma all_prenex [metric_prenex]:
   "\<And>P Q. (\<forall>x. P x) \<and> Q \<equiv> \<forall>x. (P x \<and> Q)"
   "\<And>P Q. P \<and> (\<forall>x. Q x) \<equiv> \<forall>x. (P \<and> Q x)"
   "\<And>P Q. (\<forall>x. P x) \<or> Q \<equiv> \<forall>x. (P x \<or> Q)"
   "\<And>P Q. P \<or> (\<forall>x. Q x) \<equiv> \<forall>x. (P \<or> Q x)"
   "\<And>P. \<not>(\<forall>x. P x) \<equiv> \<exists>x. \<not>P x"
   by simp_all
 
 lemma nnf_thms [metric_nnf]:
   "(\<not> (P \<and> Q)) = (\<not> P \<or> \<not> Q)"
   "(\<not> (P \<or> Q)) = (\<not> P \<and> \<not> Q)"
   "(P \<longrightarrow> Q) = (\<not> P \<or> Q)"
   "(P = Q) \<longleftrightarrow> (P \<or> \<not> Q) \<and> (\<not> P \<or> Q)"
   "(\<not> (P = Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q) \<and> (P \<or> Q)"
   "(\<not> \<not> P) = P"
   by blast+
 
 lemmas nnf_simps = nnf_thms linorder_not_less linorder_not_le
 declare nnf_simps[metric_nnf]
 
 lemma Sup_insert_insert:
   fixes a::real
   shows "Sup (insert a (insert b s)) = Sup (insert (max a b) s)"
   by (simp add: Sup_real_def)
 
 lemma real_abs_dist: "\<bar>dist x y\<bar> = dist x y"
   by simp
 
 lemma maxdist_thm [THEN HOL.eq_reflection]:
   assumes "finite s" "x \<in> s" "y \<in> s"
   defines "\<And>a. f a \<equiv> \<bar>dist x a - dist a y\<bar>"
   shows "dist x y = Sup (f ` s)"
 proof -
   have "dist x y \<le> Sup (f ` s)"
   proof -
     have "finite (f ` s)"
       by (simp add: \<open>finite s\<close>)
     moreover have "\<bar>dist x y - dist y y\<bar> \<in> f ` s"
       by (metis \<open>y \<in> s\<close> f_def imageI)
     ultimately show ?thesis
       using le_cSup_finite by simp
   qed
   also have "Sup (f ` s) \<le> dist x y"
     using \<open>x \<in> s\<close> cSUP_least[of s f] abs_dist_diff_le
     unfolding f_def
     by blast
   finally show ?thesis .
 qed
 
 theorem metric_eq_thm [THEN HOL.eq_reflection]:
   "x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>a\<in>s. dist x a = dist y a)"
   by auto
 
 ML_file "metricarith.ml"
 
 method_setup metric = \<open>
   Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac)
 \<close> "prove simple linear statements in metric spaces (\<forall>\<exists>\<^sub>p fragment)"
 
 end
\ No newline at end of file
diff --git a/src/HOL/Analysis/document/root.bib b/src/HOL/Analysis/document/root.bib
--- a/src/HOL/Analysis/document/root.bib
+++ b/src/HOL/Analysis/document/root.bib
@@ -1,11 +1,26 @@
 @article{dugundji,
   author	= {J. Dugundji},
   title		= {An extension of {Tietze's} theorem},
   journal	= {Pacific J. Math.},
   pages		= {353-367},
   volume  = 1,
   number  = 3,
   year    = 1951,
   url     = {https://projecteuclid.org/euclid.pjm/1103052106}}
 
+@article{DBLP:journals/jar/Maggesi18,
+  author    = {Marco Maggesi},
+  title     = {A Formalization of Metric Spaces in {HOL} Light},
+  journal   = {J. Autom. Reasoning},
+  volume    = {60},
+  number    = {2},
+  pages     = {237--254},
+  year      = {2018},
+  url       = {https://doi.org/10.1007/s10817-017-9412-x},
+  doi       = {10.1007/s10817-017-9412-x},
+  timestamp = {Thu, 25 Jan 2018 11:13:11 +0100},
+  biburl    = {https://dblp.org/rec/bib/journals/jar/Maggesi18},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @misc{dummy}