isabelle: src/CCL/gfp.thy@d1bf9ca9008d (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: HOL/gfp.thy
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
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	Greatest fixed points
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Gfp = Lfp +
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	consts gfp :: "['a set=>'a set] => 'a set"
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	(greatest fixed point)
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	gfp_def "gfp(f) == Union({u. u <= f(u)})"
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	end