equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Option2 imports Main begin |
2 theory Option2 imports Main begin |
3 hide const None Some |
3 hide_const None Some |
4 hide type option |
4 hide_type option |
5 (*>*) |
5 (*>*) |
6 |
6 |
7 text{*\indexbold{*option (type)}\indexbold{*None (constant)}% |
7 text{*\indexbold{*option (type)}\indexbold{*None (constant)}% |
8 \indexbold{*Some (constant)} |
8 \indexbold{*Some (constant)} |
9 Our final datatype is very simple but still eminently useful: |
9 Our final datatype is very simple but still eminently useful: |