src/HOLCF/ex/Coind.thy
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/ex/Coind.thy	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,33 +0,0 @@
     1.4 -(*  Title: 	FOCUS/ex/Coind.thy
     1.5 -    ID:         $ $
     1.6 -    Author: 	Franz Regensburger
     1.7 -    Copyright   1993 195 Technische Universitaet Muenchen
     1.8 -
     1.9 -Example for co-induction on streams
    1.10 -*)
    1.11 -
    1.12 -Coind = Stream + Dnat +
    1.13 -
    1.14 -
    1.15 -consts
    1.16 -
    1.17 -	nats		:: "dnat stream"
    1.18 -	from		:: "dnat  dnat stream"
    1.19 -
    1.20 -defs
    1.21 -	nats_def	"nats  fix`(h.dzero&&(smap`dsucc`h))"
    1.22 -
    1.23 -	from_def	"from  fix`(h n.n&&(h`(dsucc`n)))"
    1.24 -
    1.25 -end
    1.26 -
    1.27 -(*
    1.28 -		smap`f` = 
    1.29 -	x  smap`f`(x&&xs) = (f`x)&&(smap`f`xs)
    1.30 -
    1.31 -		nats = dzero&&(smap`dsucc`nats)
    1.32 -
    1.33 -		from`n = n&&(from`(dsucc`n))
    1.34 -*)
    1.35 -
    1.36 -