--- a/src/HOL/Real/HahnBanach/document/root.tex Mon Jul 17 13:58:18 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Mon Jul 17 13:59:10 2000 +0200
@@ -1,5 +1,5 @@
-
-\documentclass[11pt,a4paper,twoside]{article}
+\documentclass[10pt,a4paper,twoside]{article}
+%\documentclass[11pt,a4paper,twoside]{article}
\usepackage{latexsym,theorem}
\usepackage{isabelle,isabellesym,bbb}
@@ -34,7 +34,7 @@
\section{Preface}
This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
-the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
+the informal presentation given in the textbook \cite[{\S} 36]{Heuser:1986}.
Another formal proof of the same theorem has been done in Mizar
\cite{Nowak:1993}. A general overview of the relevance and history of the
Hahn-Banach Theorem is given in \cite{Narici:1996}.
@@ -66,6 +66,7 @@
\input{HahnBanachSupLemmas.tex}
\input{HahnBanachExtLemmas.tex}
+\input{HahnBanachLemmas.tex}
\clearpage
\part {The Main Proof}