diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/Misc/document/arith2.tex
--- a/doc-src/TutorialI/Misc/document/arith2.tex	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/arith2.tex	Mon Aug 21 19:17:07 2000 +0200
@@ -1,6 +1,6 @@
 \begin{isabelle}%
-\isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline
-\isacommand{by}(arith)\isanewline
+\isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline
 \end{isabelle}%
 %%% Local Variables:
 %%% mode: latex