| changeset 9541 | d17c0b34d5c8 |
| parent 9458 | c613cd06d5cf |
| child 9673 | 1b2d4f995b13 |
--- 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: