src/HOLCF/explicit_domains/Coind.thy

-(*  Title: 	HOLCF/Coind.thy
+(*  Title:      HOLCF/Coind.thy
     ID:         $Id$
-    Author: 	Franz Regensburger
+    Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
 Example for co-induction on streams
 *)
 
 Coind = Stream2 +
 
 
 consts
 
-	nats		:: "dnat stream"
-	from		:: "dnat -> dnat stream"
+        nats            :: "dnat stream"
+        from            :: "dnat -> dnat stream"
 
 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
+                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))
 *)