src/HOLCF/explicit_domains/Stream2.thy
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Stream2.thy	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,31 +0,0 @@
     1.4 -(* 
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
    1.10 -
    1.11 -Additional constants for stream
    1.12 -*)
    1.13 -
    1.14 -Stream2 = Stream +
    1.15 -
    1.16 -consts
    1.17 -
    1.18 -smap            :: "('a -> 'b) -> 'a stream -> 'b stream"
    1.19 -
    1.20 -defs
    1.21 -
    1.22 -smap_def
    1.23 -  "smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
    1.24 -
    1.25 -
    1.26 -end
    1.27 -      
    1.28 -
    1.29 -(*
    1.30 -                smap`f`UU = UU
    1.31 -      x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
    1.32 -
    1.33 -*)
    1.34 -