isabelle: src/HOLCF/explicit_domains/Dagstuhl.thy@8d42a7bccf0b (annotated)

1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	1	(* $Id$ *)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	3
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4	Dagstuhl = Stream2 +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	consts
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	7	y :: "'a"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8	YS :: "'a stream"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	9	YYS :: "'a stream"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	10
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11	defs
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13	YS_def "YS == fix`(LAM x. scons`y`x)"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14	YYS_def "YYS == fix`(LAM z. scons`y`(scons`y`z))"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16	end
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17