| changeset 21404 | eb85850d3eb7 |
| parent 19763 | ec18656a2c10 |
| child 25135 | 4f8176c940cf |
--- a/src/HOLCF/ex/Dagstuhl.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOLCF/ex/Dagstuhl.thy Fri Nov 17 02:20:03 2006 +0100 @@ -8,9 +8,11 @@ y :: "'a" definition - YS :: "'a stream" + YS :: "'a stream" where "YS = fix$(LAM x. y && x)" - YYS :: "'a stream" + +definition + YYS :: "'a stream" where "YYS = fix$(LAM z. y && y && z)" lemma YS_def2: "YS = y && YS"