author wenzelm Sat, 20 Oct 2001 20:20:21 +0200 changeset 11851 d190028f43c5 parent 11850 cdfc3fce577e child 11852 a528a716a312
include document graph; tuned;
--- 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}