--- a/src/HOL/Gfp.thy Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Gfp.thy Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
Greatest fixed points (requires Lfp too!)
*)
-theory Gfp = Lfp:
+theory Gfp
+import Lfp
+begin
constdefs
gfp :: "['a set=>'a set] => 'a set"