--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Sep 11 18:00:47 2000 +0200
@@ -1,14 +1,13 @@
%
\begin{isabellebody}%
+\def\isabellecontext{natsum}%
%
\begin{isamarkuptext}%
\noindent
In particular, there are \isa{case}-expressions, for example
-%
\begin{isabelle}%
\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
-\end{isabelle}%
-
+\end{isabelle}
primitive recursion, for example%
\end{isamarkuptext}%
\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline