isabelle: src/HOLCF/ex/Fix2.thy@a389e5892691 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/ex/Fix2.thy
1274 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
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	Show that fix is the unique least fixed-point operator.
12036 49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	6	From axioms gix1_def,gix2_def it follows that fix = gix
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	theory Fix2
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	imports HOLCF
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	11	begin
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13	consts
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	gix :: "('a->'a)->'a"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	16	axioms
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	gix1_def: "F$(gix$F) = gix$F"
94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	18	gix2_def: "F$y=y ==> gix$F << y"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	19
17291 94f6113fe9ed converted to Isar theory format; wenzelm parents: 14981 diff changeset	20	ML {* use_legacy_bindings (the_context ()) *}
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22	end

author	obua
	Sat, 17 Sep 2005 11:49:29 +0200
changeset 17444	a389e5892691
parent 17291	94f6113fe9ed
child 19742	86f21beabafc
permissions	-rw-r--r--