src/HOL/Analysis/document/root.bib
author wenzelm
Sun, 25 Aug 2024 23:19:33 +0200
changeset 80772 39641d8bd422
parent 79957 ef635b035561
permissions -rw-r--r--
merged
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
79957
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    34
@book{Lang_1993, 
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    35
	place={New York}, 
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    36
	title={Real and Functional Analysis}, 
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    37
	publisher={Springer}, 
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    38
	author={Lang, Serge}, 
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    39
	year={1993},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    40
	isbn={978-1-4612-0897-6}
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    41
} 
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    42
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    43
@book{engelking_1989,
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    44
	title={General Topology},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    45
	author={Engelking, R.},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    46
	isbn={978-3-8853-8006-1},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    47
	series={Sigma series in pure mathematics},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    48
	url={https://books.google.com.tr/books?id=K3spAQAAMAAJ},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    49
	year={1989},
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    50
	publisher={Heldermann}
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    51
}
ef635b035561 proper bib entries (amending 82aaa0d8fc3b);
wenzelm
parents: 74475
diff changeset
    52
69519
0563419bf022 added bib-file
nipkow
parents:
diff changeset
    53
@misc{dummy}