src/HOLCF/Stream2.thy
changeset 1274 ea0668a1c0ba
parent 1273 6960ec882bca
child 1275 5d68da443a9f
--- a/src/HOLCF/Stream2.thy	Fri Oct 06 16:17:08 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(*  Title: 	HOLCF/stream2.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Additional constants for stream
-*)
-
-Stream2 = Stream +
-
-consts
-
-smap		:: "('a -> 'b) -> 'a stream -> 'b stream"
-
-defs
-
-smap_def
-  "smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
-
-
-end
-      
-
-(*
-		smap`f`UU = UU
-      x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
-
-*)
-