(*  Title:      CCL/Gfp.thy
    ID:         $Id: Gfp.thy,v 1.3 2005/09/17 15:35:27 wenzelm Exp $
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

header {* Greatest fixed points *}

theory Gfp
imports Lfp
begin

constdefs
  gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
  "gfp(f) == Union({u. u <= f(u)})"

ML {* use_legacy_bindings (the_context ()) *}

end