--- a/src/HOL/Gfp.thy Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Gfp.thy Thu May 18 11:43:57 2000 +0200
@@ -8,12 +8,8 @@
Gfp = Lfp +
-global
-
constdefs
gfp :: ['a set=>'a set] => 'a set
"gfp(f) == Union({u. u <= f(u)})" (*greatest fixed point*)
-local
-
end