--- a/src/HOL/Analysis/Metric_Arith.thy Sun Oct 27 17:26:50 2019 +0100
+++ b/src/HOL/Analysis/Metric_Arith.thy Sun Oct 27 12:09:07 2019 -0400
@@ -8,6 +8,12 @@
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
--- a/src/HOL/Analysis/document/root.bib Sun Oct 27 17:26:50 2019 +0100
+++ b/src/HOL/Analysis/document/root.bib Sun Oct 27 12:09:07 2019 -0400
@@ -8,4 +8,19 @@
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}