isabelle: src/CCL/Lfp.thy@b2877e230b07 (annotated)

17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	1	(* Title: CCL/Lfp.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
17456 bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	7	header {* The Knaster-Tarski Theorem *}
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	8
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	9	theory Lfp
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	10	imports Set
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	11	uses "subset.ML" "equalities.ML" "mono.ML"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	12	begin
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	13
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	14	constdefs
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	15	lfp :: "['a set=>'a set] => 'a set" (least fixed point)
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	16	"lfp(f) == Inter({u. f(u) <= u})"
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	17
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	18	ML {* use_legacy_bindings (the_context ()) *}
bcf7544875b2 converted to Isar theory format; wenzelm parents: 1474 diff changeset	19
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	20	end

author	huffman
	Thu, 13 Apr 2006 23:15:44 +0200
changeset 19440	b2877e230b07
parent 17456	bcf7544875b2
child 20140	98acc6d0fab6
permissions	-rw-r--r--