diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/document/root.tex
--- 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}