# HG changeset patch
# User immler
# Date 1572192547 14400
# Node ID 420359ba6acde48aa7e65af504f5b2f12dee4c11
# Parent  f140135ff375be4866ebb91b5fd43986dd977128
documented reference

diff -r f140135ff375 -r 420359ba6acd src/HOL/Analysis/Metric_Arith.thy
--- 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
diff -r f140135ff375 -r 420359ba6acd src/HOL/Analysis/document/root.bib
--- 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}