src/HOL/Analysis/document/root.bib
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 74475 409ca22dee4c
child 79957 ef635b035561
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69519
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     1
@article{dugundji,
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     2
  author	= {J. Dugundji},
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     3
  title		= {An extension of {Tietze's} theorem},
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     4
  journal	= {Pacific J. Math.},
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     5
  pages		= {353-367},
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     6
  volume  = 1,
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     7
  number  = 3,
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     8
  year    = 1951,
0563419bf022 added bib-file
nipkow
parents:
diff changeset
     9
  url     = {https://projecteuclid.org/euclid.pjm/1103052106}}
0563419bf022 added bib-file
nipkow
parents:
diff changeset
    10
70953
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    11
@article{DBLP:journals/jar/Maggesi18,
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    12
  author    = {Marco Maggesi},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    13
  title     = {A Formalization of Metric Spaces in {HOL} Light},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    14
  journal   = {J. Autom. Reasoning},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    15
  volume    = {60},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    16
  number    = {2},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    17
  pages     = {237--254},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    18
  year      = {2018},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    19
  url       = {https://doi.org/10.1007/s10817-017-9412-x},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    20
  doi       = {10.1007/s10817-017-9412-x},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    21
  timestamp = {Thu, 25 Jan 2018 11:13:11 +0100},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    22
  biburl    = {https://dblp.org/rec/bib/journals/jar/Maggesi18},
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    23
  bibsource = {dblp computer science bibliography, https://dblp.org}
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    24
}
420359ba6acd documented reference
immler
parents: 69519
diff changeset
    25
74475
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    26
@book{conway2013course,
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    27
  title={A course in functional analysis},
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    28
  author={Conway, John B},
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    29
  volume={96},
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    30
  year={2013},
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    31
  publisher={Springer Science \& Business Media}
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    32
}
409ca22dee4c new notion of infinite sums in HOL-Analysis, ordering on complex numbers
eberlm <eberlm@in.tum.de>
parents: 70953
diff changeset
    33
69519
0563419bf022 added bib-file
nipkow
parents:
diff changeset
    34
@misc{dummy}