diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/natsum.thy --- 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 *}