src/HOLCF/ex/Coind.thy

--- a/src/HOLCF/ex/Coind.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/ex/Coind.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -11,27 +11,23 @@
 
 consts
 
-nats		:: "dnat stream"
-from		:: "dnat -> dnat stream"
+	nats		:: "dnat stream"
+	from		:: "dnat -> dnat stream"
 
-rules
+defs
+	nats_def	"nats == fix`(LAM h.scons`dzero`(smap`dsucc`h))"
 
-nats_def	"nats = fix[LAM h.scons[dzero][smap[dsucc][h]]]"
-
-from_def	"from = fix[LAM h n.scons[n][h[dsucc[n]]]]"
+	from_def	"from == fix`(LAM h n.scons`n`(h`(dsucc`n)))"
 
 end
 
 (*
-
-		smap[f][UU] = UU
-      x~=UU --> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]
+		smap`f`UU = UU
+      x~=UU --> smap`f`(scons`x`xs) = scons`(f`x)`(smap`f`xs)
 
-		nats = scons[dzero][smap[dsucc][nats]]
+		nats = scons`dzero`(smap`dsucc`nats)
 
-		from[n] = scons[n][from[dsucc[n]]]
-
-
+		from`n = scons`n`(from`(dsucc`n))
 *)