changeset 66364 | fa3247e6ee4b |
parent 63648 | f9f3006a5579 |
child 67091 | 1393c2340eec |
66363:8aca34dbe195 | 66364:fa3247e6ee4b |
---|---|
3 *) |
3 *) |
4 |
4 |
5 section \<open>Datatype option\<close> |
5 section \<open>Datatype option\<close> |
6 |
6 |
7 theory Option |
7 theory Option |
8 imports Lifting Finite_Set |
8 imports Lifting |
9 begin |
9 begin |
10 |
10 |
11 datatype 'a option = |
11 datatype 'a option = |
12 None |
12 None |
13 | Some (the: 'a) |
13 | Some (the: 'a) |