isabelle: src/HOL/Lfp.thy@197e00ce3f20 (annotated)

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	1	(* Title: HOL/Lfp.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6	The Knaster-Tarski Theorem
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
15131 c69542757a4d New theory header syntax. nipkow parents: 14169 diff changeset	9	theory Lfp
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	10	imports Product_Type
15131 c69542757a4d New theory header syntax. nipkow parents: 14169 diff changeset	11	begin
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	12
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	13	constdefs
14169 0590de71a016 Converted to new style theories. skalberg parents: 11609 diff changeset	14	lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	15	"lfp(f) == Inter({u. f(u) <= u})" (least fixed point)
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	16
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	17	end

author	nipkow
	Fri, 10 Sep 2004 00:19:15 +0200
changeset 15195	197e00ce3f20
parent 15140	322485b816ac
child 15386	06757406d8cf
permissions	-rw-r--r--