
diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/arith2.tex
--- a/doc-src/TutorialI/Misc/document/arith2.tex	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Sun Aug 06 15:26:53 2000 +0200
@@ -1,5 +1,5 @@
 \begin{isabelle}%
-\isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline
+\isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline
 \isacommand{by}(arith)\isanewline
 \end{isabelle}%
 %%% Local Variables:




