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}