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