--- a/src/HOL/Real/HahnBanach/document/root.tex Thu Jul 29 12:15:53 2004 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Thu Jul 29 16:14:06 2004 +0200
@@ -1,4 +1,3 @@
-
\documentclass[10pt,a4paper,twoside]{article}
\usepackage{graphicx}
\usepackage{latexsym,theorem}
@@ -37,10 +36,10 @@
\section{Preface}
This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
-the informal presentation given in the textbook \cite[{\S} 36]{Heuser:1986}.
+the informal presentation given in Heuser's textbook \cite[{\S} 36]{Heuser:1986}.
Another formal proof of the same theorem has been done in Mizar
\cite{Nowak:1993}. A general overview of the relevance and history of the
-Hahn-Banach Theorem is given in \cite{Narici:1996}.
+Hahn-Banach Theorem is given by Narici and Beckenstein \cite{Narici:1996}.
\medskip The document is structured as follows. The first part contains
definitions of basic notions of linear algebra: vector spaces, subspaces,