--- a/src/HOLCF/ex/coind.thy Sat Apr 05 17:03:38 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(* Title: HOLCF/coind.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Example for co-induction on streams
-*)
-
-Coind = Stream2 +
-
-
-consts
-
-nats :: "dnat stream"
-from :: "dnat -> dnat stream"
-
-rules
-
-nats_def "nats = fix[LAM h.scons[dzero][smap[dsucc][h]]]"
-
-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]]
-
- nats = scons[dzero][smap[dsucc][nats]]
-
- from[n] = scons[n][from[dsucc[n]]]
-
-
-*)
-
-