isabelle: src/HOLCF/ex/Fix2.thy@3e47692e3a3e (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
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	4	Copyright 1995 Technische Universitaet Muenchen
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6	Show that fix is the unique least fixed-point operator.
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	7	From axioms gix1_def,gix2_def it follows that fix = gix
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
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	11	Fix2 = Fix +
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	12
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	13	consts
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15	gix :: "('a->'a)->'a"
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	17	rules
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	18
10835 f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	19	gix1_def "F$(gix$F) = gix$F"
f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	20	gix2_def "F$y=y ==> gix$F << y"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22	end

author	wenzelm
	Thu, 15 Feb 2001 17:18:54 +0100
changeset 11145	3e47692e3a3e
parent 10835	f4745d77e620
child 12036	49f6c49454c2
permissions	-rw-r--r--