diff -r bf399f3bd7dc -r 36cb5fb8188c src/HOL/Real/HahnBanach/document/root.tex
--- a/src/HOL/Real/HahnBanach/document/root.tex	Thu Aug 29 16:08:30 2002 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Thu Aug 29 16:08:32 2002 +0200
@@ -52,7 +52,7 @@
 as follows.
 
 \begin{center}
-  \includegraphics[scale=0.7]{session_graph}  
+  \includegraphics[scale=0.5]{session_graph}  
 \end{center}
 
 \clearpage