isabelle: src/HOLCF/ex/Dagstuhl.thy@c9c6ae9e8b88 (annotated)

2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	1	(* $Id$ *)
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	2
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	3	theory Dagstuhl
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	4	imports Stream
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	5	begin
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	6
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	7	consts
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	8	y :: "'a"
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	9
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	10	constdefs
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	11	YS :: "'a stream"
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	12	"YS == fix$(LAM x. y && x)"
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	13	YYS :: "'a stream"
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	14	"YYS == fix$(LAM z. y && y && z)"
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	15
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	16	ML {* use_legacy_bindings (the_context ()) *}
94f6113fe9ed converted to Isar theory format; wenzelm parents: 10835 diff changeset	17
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	18	end
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	19

author	paulson
	Mon, 23 Jan 2006 11:38:43 +0100
changeset 18752	c9c6ae9e8b88
parent 17291	94f6113fe9ed
child 19742	86f21beabafc
permissions	-rw-r--r--