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 \isamarkupfalse% |
4 % |
5 % |
5 \isadelimtheory |
6 \isadelimtheory |
6 % |
7 % |
7 \endisadelimtheory |
8 \endisadelimtheory |
8 % |
9 % |
9 \isatagtheory |
10 \isatagtheory |
10 \isamarkupfalse% |
|
11 % |
11 % |
12 \endisatagtheory |
12 \endisatagtheory |
13 {\isafoldtheory}% |
13 {\isafoldtheory}% |
14 % |
14 % |
15 \isadelimtheory |
15 \isadelimtheory |
16 % |
16 % |
17 \endisadelimtheory |
17 \endisadelimtheory |
18 \isamarkupfalse% |
|
19 \isamarkupfalse% |
|
20 % |
18 % |
21 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
22 \indexbold{*option (type)}\indexbold{*None (constant)}% |
20 \indexbold{*option (type)}\indexbold{*None (constant)}% |
23 \indexbold{*Some (constant)} |
21 \indexbold{*Some (constant)} |
24 Our final datatype is very simple but still eminently useful:% |
22 Our final datatype is very simple but still eminently useful:% |
43 \isadelimtheory |
41 \isadelimtheory |
44 % |
42 % |
45 \endisadelimtheory |
43 \endisadelimtheory |
46 % |
44 % |
47 \isatagtheory |
45 \isatagtheory |
48 \isamarkupfalse% |
|
49 % |
46 % |
50 \endisatagtheory |
47 \endisatagtheory |
51 {\isafoldtheory}% |
48 {\isafoldtheory}% |
52 % |
49 % |
53 \isadelimtheory |
50 \isadelimtheory |