equal
deleted
inserted
replaced
1 (* Title: HOL/BNF/Examples/Misc_Codata.thy |
1 (* Title: HOL/BNF/Examples/Misc_Codata.thy |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
3 Author: Andrei Popescu, TU Muenchen |
3 Author: Andrei Popescu, TU Muenchen |
4 Copyright 2012 |
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright 2012, 2013 |
5 |
6 |
6 Miscellaneous codatatype declarations. |
7 Miscellaneous codatatype declarations. |
7 *) |
8 *) |
8 |
9 |
9 header {* Miscellaneous Codatatype Declarations *} |
10 header {* Miscellaneous Codatatype Declarations *} |
13 begin |
14 begin |
14 |
15 |
15 codatatype simple = X1 | X2 | X3 | X4 |
16 codatatype simple = X1 | X2 | X3 | X4 |
16 |
17 |
17 codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit |
18 codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit |
|
19 |
|
20 codatatype simple'' = X1'' nat int | X2'' |
18 |
21 |
19 codatatype 'a stream = Stream 'a "'a stream" |
22 codatatype 'a stream = Stream 'a "'a stream" |
20 |
23 |
21 codatatype 'a mylist = MyNil | MyCons 'a "'a mylist" |
24 codatatype 'a mylist = MyNil | MyCons 'a "'a mylist" |
22 |
25 |