--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 21 19:17:07 2000 +0200
@@ -6,22 +6,22 @@
\begin{quote}
\begin{isabelle}%
-case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m}
+case\ \mbox{n}\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m}
\end{isabelle}%
\end{quote}
primitive recursion, for example%
\end{isamarkuptext}%
-\isacommand{consts}\ sum\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{primrec}\ {"}sum\ 0\ =\ 0{"}\isanewline
-\ \ \ \ \ \ \ \ {"}sum\ (Suc\ n)\ =\ Suc\ n\ +\ sum\ n{"}%
+\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
and induction, for example%
\end{isamarkuptext}%
-\isacommand{lemma}\ {"}sum\ n\ +\ sum\ n\ =\ n*(Suc\ n){"}\isanewline
-\isacommand{apply}(induct\_tac\ n)\isanewline
-\isacommand{by}(auto)\isanewline
+\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
+\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex