changeset 9644 | 6b0b6b471855 |
parent 9541 | d17c0b34d5c8 |
child 9673 | 1b2d4f995b13 |
--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Aug 17 21:07:25 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Aug 18 10:34:08 2000 +0200 @@ -6,7 +6,7 @@ \begin{quote} \begin{isabelle}% -case\ n\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ m\ {\isasymRightarrow}\ m +case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} \end{isabelle}% \end{quote}