src/HOLCF/ex/Dagstuhl.thy
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
+