isabelle: src/HOLCF/ex/Fix2.thy@00b9a5073b01 (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
12036 49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
12036 49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	6	Show that fix is the unique least fixed-point operator.
49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	7	From axioms gix1_def,gix2_def it follows that fix = gix
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	8	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	9
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	10	Fix2 = Fix +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12	consts
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14	gix :: "('a->'a)->'a"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16	rules
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17
10835 f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	18	gix1_def "F$(gix$F) = gix$F"
f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	19	gix2_def "F$y=y ==> gix$F << y"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21	end

author	paulson
	Mon, 26 Apr 2004 11:15:56 +0200
changeset 14669	00b9a5073b01
parent 12036	49f6c49454c2
child 14981	e73f8140af78
permissions	-rw-r--r--