--- a/src/CCL/Gfp.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Gfp.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,14 +1,19 @@
-(* Title: HOL/gfp.thy
+(* Title: CCL/Gfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-Greatest fixed points
*)
-Gfp = Lfp +
-consts gfp :: "['a set=>'a set] => 'a set"
-rules
- (*greatest fixed point*)
- gfp_def "gfp(f) == Union({u. u <= f(u)})"
+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