src/HOL/Real/HahnBanach/document/root.bib
author fleuriot
Thu, 01 Jun 2000 11:22:27 +0200
changeset 9013 9dd0274f76af
parent 7927 b50446a33c16
permissions -rw-r--r--
Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7927
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     1
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     2
@Book{Heuser:1986,
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     3
  author = 	 {H. Heuser},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     4
  title = 	 {Funktionalanalysis: Theorie und Anwendung},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     5
  publisher = 	 {Teubner},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     6
  year = 	 1986
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     7
}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     8
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
     9
@InCollection{Narici:1996,
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    10
  author = 	 {L. Narici and E. Beckenstein},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    11
  title = 	 {The {Hahn-Banach Theorem}: The Life and Times},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    12
  booktitle = 	 {Topology Atlas},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    13
  publisher =	 {York University, Toronto, Ontario, Canada},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    14
  year =	 1996,
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    15
  note =	 {\url{http://at.yorku.ca/topology/preprint.htm} and
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    16
                  \url{http://at.yorku.ca/p/a/a/a/16.htm}}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    17
}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    18
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    19
@Article{Nowak:1993,
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    20
  author =       {B. Nowak and A. Trybulec},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    21
  title =	 {{Hahn-Banach} Theorem},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    22
  journal =      {Journal of Formalized Mathematics},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    23
  year =         {1993},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    24
  volume =       {5},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    25
  institution =  {University of Bialystok},
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    26
  note =         {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents:
diff changeset
    27
}