author | wenzelm |
Thu, 29 Aug 2002 16:08:32 +0200 | |
changeset 13548 | 36cb5fb8188c |
parent 13547 | bf399f3bd7dc |
child 13549 | f1522b892a4c |
--- 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