src/HOLCF/stream2.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 297 5ef75ff3baeb
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/stream2.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Additional constants for stream
     7 *)
     8 
     9 Stream2 = Stream +
    10 
    11 consts
    12 
    13 smap		:: "('a -> 'b) -> 'a stream -> 'b stream"
    14 
    15 rules
    16 
    17 smap_def
    18   "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
    19 
    20 
    21 end
    22       
    23 
    24 (*
    25 		smap[f][UU] = UU
    26       x~=UU --> smap[f][scons[x][xs]] = scons[f[x]][smap[f][xs]]
    27 
    28 *)
    29