--- a/doc-src/TutorialI/Misc/document/Option2.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Tue Jul 17 13:46:21 2001 +0200
@@ -3,7 +3,8 @@
\def\isabellecontext{Option{\isadigit{2}}}%
%
\begin{isamarkuptext}%
-\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+\indexbold{*option (type)}\indexbold{*None (constant)}%
+\indexbold{*Some (constant)}
Our final datatype is very simple but still eminently useful:%
\end{isamarkuptext}%
\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%