changeset 2570 | 24d7e8fb8261 |
child 10835 | f4745d77e620 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/ex/Dagstuhl.thy Fri Jan 31 16:56:32 1997 +0100 @@ -0,0 +1,17 @@ +(* $Id$ *) + + +Dagstuhl = Stream + + +consts + y :: "'a" + YS :: "'a stream" + YYS :: "'a stream" + +defs + +YS_def "YS == fix`(LAM x. y && x)" +YYS_def "YYS == fix`(LAM z. y && y && z)" + +end +