| changeset 16417 | 9bc16273c2d4 |
| parent 15905 | 0a4cc9b113c7 |
| child 35416 | d8d7d1b785af |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Option2 = Main: |
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)}% |