--- a/src/HOL/Real/HahnBanach/document/root.tex Sat Aug 19 12:44:20 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Sat Aug 19 12:44:39 2000 +0200
@@ -4,6 +4,7 @@
\usepackage{latexsym,theorem}
\usepackage{isabelle,isabellesym,bbb}
\usepackage{pdfsetup} %last one!
+\urlstyle{rm}
\input{notation}
@@ -13,10 +14,8 @@
\pagenumbering{arabic}
\title{The Hahn-Banach Theorem for Real Vector Spaces}
-
\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
\maketitle
-\maketitle
\begin{abstract}
The Hahn-Banach Theorem is one of the most fundamental results in functional