src/HOL/Gfp.thy

--- a/src/HOL/Gfp.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Gfp.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -7,8 +7,9 @@
 *)
 
 Gfp = Lfp +
-consts gfp :: ['a set=>'a set] => 'a set
-defs
- (*greatest fixed point*)
- gfp_def "gfp(f) == Union({u. u <= f(u)})"
+
+constdefs
+  gfp :: ['a set=>'a set] => 'a set
+  "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
+
 end