| changeset 9792 | bbefb6ce5cb2 |
| parent 9541 | d17c0b34d5c8 |
| child 9834 | 109b11c4e77e |
--- a/doc-src/TutorialI/Misc/natsum.thy Fri Sep 01 18:29:52 2000 +0200 +++ b/doc-src/TutorialI/Misc/natsum.thy Fri Sep 01 19:09:44 2000 +0200 @@ -2,7 +2,7 @@ theory natsum = Main:; (*>*) text{*\noindent -In particular, there are \isa{case}-expressions, for example +In particular, there are @{text"case"}-expressions, for example \begin{quote} @{term[display]"case n of 0 => 0 | Suc m => m"} \end{quote}