changeset 9834 | 109b11c4e77e |
parent 9792 | bbefb6ce5cb2 |
child 10171 | 59d6633835fa |
--- a/doc-src/TutorialI/Misc/natsum.thy Mon Sep 04 21:20:14 2000 +0200 +++ b/doc-src/TutorialI/Misc/natsum.thy Tue Sep 05 09:03:17 2000 +0200 @@ -3,9 +3,7 @@ (*>*) text{*\noindent In particular, there are @{text"case"}-expressions, for example -\begin{quote} @{term[display]"case n of 0 => 0 | Suc m => m"} -\end{quote} primitive recursion, for example *}