| changeset 9792 | bbefb6ce5cb2 |
| parent 9722 | a5f86aed785b |
| child 9834 | 109b11c4e77e |
--- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Sep 01 18:29:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Fri Sep 01 19:09:44 2000 +0200 @@ -7,7 +7,7 @@ \begin{quote} \begin{isabelle}% -case\ \mbox{n}\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} +case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m \end{isabelle}% \end{quote}