equal
deleted
inserted
replaced
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
2 (* Author: Lukas Bulwahn, TU Muenchen *) |
3 |
3 |
4 header {* Depth-Limited Sequences with failure element *} |
4 header {* Depth-Limited Sequences with failure element *} |
5 |
5 |
6 theory New_DSequence |
6 theory New_DSequence |
7 imports Random_Sequence |
7 imports DSequence |
8 begin |
8 begin |
9 |
9 |
10 subsection {* Positive Depth-Limited Sequence *} |
10 subsection {* Positive Depth-Limited Sequence *} |
11 |
11 |
12 type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence" |
12 type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence" |