changeset 299 | febeb36a4ba4 |
child 896 | 56b9c2626e81 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/ex/Dagstuhl.thy Thu Mar 24 13:45:06 1994 +0100 @@ -0,0 +1,17 @@ +(* + ID: $ $ +*) + +Dagstuhl = Stream2 + + +consts + YS :: "'a stream" + YYS :: "'a stream" + +rules + +YS_def "YS = fix[LAM x. scons[y][x]]" +YYS_def "YYS = fix[LAM z. scons[y][scons[y][z]]]" + +end +