src/HOL/Analysis/document/root.bib

more zproofs;

@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}
}

@book{conway2013course,
  title={A course in functional analysis},
  author={Conway, John B},
  volume={96},
  year={2013},
  publisher={Springer Science \& Business Media}
}

@misc{dummy}