--- a/Gfp.thy Thu Nov 24 20:11:40 1994 +0100 +++ b/Gfp.thy Thu Nov 24 20:31:09 1994 +0100 @@ -8,7 +8,7 @@ Gfp = Lfp + consts gfp :: "['a set=>'a set] => 'a set" -rules +defs (*greatest fixed point*) gfp_def "gfp(f) == Union({u. u <= f(u)})" end