# HG changeset patch
# User bauerg
# Date 963835150 -7200
# Node ID cc0fd5226bb70ce0e54ae1ec672a633a41f167f3
# Parent  153853af318b234eb1a3a34e7861d07c0ffcfe41
10pt

diff -r 153853af318b -r cc0fd5226bb7 src/HOL/Real/HahnBanach/document/root.tex
--- 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}