isabelle: src/HOL/Lfp.thy@3a5864b465e2 (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
1114 c8dfb56a7e95 Prod is now a parent of Lfp. nipkow parents: 923 diff changeset	9	Lfp = mono + Prod +
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	10
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 1558 diff changeset	11	global
eb707467f8c5 adapted to qualified names; wenzelm parents: 1558 diff changeset	12
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	13	constdefs
9c6ebfab4e05 added constdefs section clasohm parents: 1475 diff changeset	14	lfp :: ['a set=>'a set] => 'a set
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
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 1558 diff changeset	17	local
eb707467f8c5 adapted to qualified names; wenzelm parents: 1558 diff changeset	18
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	19	end

author	paulson
	Fri, 14 Jan 2000 12:17:53 +0100
changeset 8128	3a5864b465e2
parent 3947	eb707467f8c5
child 8882	9df44a4f1bf7
permissions	-rw-r--r--