equal
deleted
inserted
replaced
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
3 |
3 |
4 header {* Lazy sequences *} |
4 header {* Lazy sequences *} |
5 |
5 |
6 theory Lazy_Sequence |
6 theory Lazy_Sequence |
7 imports List Code_Numeral |
7 imports Predicate |
8 begin |
8 begin |
9 |
9 |
10 datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence" |
10 datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence" |
11 |
11 |
12 definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence" |
12 definition Lazy_Sequence :: "(unit => ('a * 'a lazy_sequence) option) => 'a lazy_sequence" |