equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Option{\isadigit{2}}}% |
3 \def\isabellecontext{Option{\isadigit{2}}}% |
4 % |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \indexbold{*option}\indexbold{*None}\indexbold{*Some} |
6 \indexbold{*option (type)}\indexbold{*None (constant)}% |
|
7 \indexbold{*Some (constant)} |
7 Our final datatype is very simple but still eminently useful:% |
8 Our final datatype is very simple but still eminently useful:% |
8 \end{isamarkuptext}% |
9 \end{isamarkuptext}% |
9 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a% |
10 \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a% |
10 \begin{isamarkuptext}% |
11 \begin{isamarkuptext}% |
11 \noindent |
12 \noindent |