isabelle: src/HOLCF/explicit_domains/Stream2.thy@51993fea433f (annotated)

1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	1	(*
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	Additional constants for stream
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	9	Stream2 = Stream +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	10
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11	consts
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	13	smap :: "('a -> 'b) -> 'a stream -> 'b stream"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15	defs
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17	smap_def
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	18	"smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	19
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21	end
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	23
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	24	(*
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	25	smap`f`UU = UU
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	26	x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	27
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	28	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	29

author	oheimb
	Wed, 18 Dec 1996 15:16:13 +0100
changeset 2445	51993fea433f
parent 1479	21eb5e156d91
child 2569	3a8604f408c9
permissions	-rw-r--r--