1.1 --- a/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 08 16:18:51 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 08 16:40:27 1999 +0200
     1.3 @@ -2,12 +2,20 @@
     1.4  \documentclass[11pt,a4paper]{article}
     1.5  \usepackage{isabelle,pdfsetup}
     1.6  
     1.7 +\input{notation}
     1.8 +
     1.9  \begin{document}
    1.10  
    1.11 -\title{The Hahn-Banach theorem for real vectorspaces}
    1.12 +\title{The Hahn-Banach Theorem for Real Vectorspaces}
    1.13  \author{Gertrud Bauer}
    1.14  \maketitle
    1.15  
    1.16 +\begin{abstract}
    1.17 +  FIXME
    1.18 +\end{abstract}
    1.19 +
    1.20 +\tableofcontents
    1.21 +
    1.22  \input{session}
    1.23  
    1.24  \end{document}