# HG changeset patch
# User wenzelm
# Date 1030630112 -7200
# Node ID 36cb5fb8188c8875ec3383e4d3b23c338661ebdf
# Parent  bf399f3bd7dc22a105eb4892be4ad059db6655e7
*** empty log message ***

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