--- a/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Fri Oct 08 16:40:27 1999 +0200
@@ -2,12 +2,20 @@
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,pdfsetup}
+\input{notation}
+
\begin{document}
-\title{The Hahn-Banach theorem for real vectorspaces}
+\title{The Hahn-Banach Theorem for Real Vectorspaces}
\author{Gertrud Bauer}
\maketitle
+\begin{abstract}
+ FIXME
+\end{abstract}
+
+\tableofcontents
+
\input{session}
\end{document}