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

1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	1	(* Title: HOL/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	The Knaster-Tarski Theorem
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Lfp = Set +
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	consts lfp :: "['a set=>'a set] => 'a set"
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	(least fixed point)
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	lfp_def "lfp(f) == Inter({u. f(u) <= u})"
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	end