| changeset 13548 | 36cb5fb8188c |
| parent 11851 | d190028f43c5 |
| child 14721 | 782932b1e931 |
--- 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