changeset 25135 | 4f8176c940cf |
parent 21404 | eb85850d3eb7 |
child 35169 | 31cbcb019003 |
25134:3d4953e88449 | 25135:4f8176c940cf |
---|---|
2 |
2 |
3 theory Dagstuhl |
3 theory Dagstuhl |
4 imports Stream |
4 imports Stream |
5 begin |
5 begin |
6 |
6 |
7 consts |
7 axiomatization |
8 y :: "'a" |
8 y :: "'a" |
9 |
9 |
10 definition |
10 definition |
11 YS :: "'a stream" where |
11 YS :: "'a stream" where |
12 "YS = fix$(LAM x. y && x)" |
12 "YS = fix$(LAM x. y && x)" |