# HG changeset patch
# User wenzelm
# Date 1003602021 -7200
# Node ID d190028f43c50ee959a803b061790756bf9c6924
# Parent  cdfc3fce577ea6c277a43632e748ed01c92bf64b
include document graph;
tuned;

diff -r cdfc3fce577e -r d190028f43c5 src/HOL/Real/HahnBanach/document/root.tex
--- a/src/HOL/Real/HahnBanach/document/root.tex	Sat Oct 20 20:19:47 2001 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Sat Oct 20 20:20:21 2001 +0200
@@ -1,6 +1,6 @@
 
 \documentclass[10pt,a4paper,twoside]{article}
-
+\usepackage{graphicx}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup} %last one!
@@ -17,7 +17,7 @@
 \pagestyle{headings}
 \pagenumbering{arabic}
 
-\title{The Hahn-Banach Theorem for Real Vector Spaces}
+\title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
 \author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
 \maketitle
 
@@ -44,12 +44,16 @@
 
 \medskip The document is structured as follows.  The first part contains
 definitions of basic notions of linear algebra: vector spaces, subspaces,
-normed spaces, continuous linearforms, norm of functions and an order on
+normed spaces, continuous linear-forms, norm of functions and an order on
 functions by domain extension.  The second part contains some lemmas about the
 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
 With these preliminaries, the main proof of the theorem (in its two versions)
-is conducted in the third part.
+is conducted in the third part.  The dependencies of individual theories are
+as follows.
 
+\begin{center}
+  \includegraphics[scale=0.7]{session_graph}  
+\end{center}
 
 \clearpage
 \part {Basic Notions}