equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Potentially infinite lists as greatest fixed-point *} |
6 header {* Potentially infinite lists as greatest fixed-point *} |
7 |
7 |
8 theory Coinductive_List |
8 theory Coinductive_List |
9 imports List |
9 imports Plain List |
10 begin |
10 begin |
11 |
11 |
12 subsection {* List constructors over the datatype universe *} |
12 subsection {* List constructors over the datatype universe *} |
13 |
13 |
14 definition "NIL = Datatype.In0 (Datatype.Numb 0)" |
14 definition "NIL = Datatype.In0 (Datatype.Numb 0)" |