--- a/src/CCL/Lfp.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/Lfp.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,14 +1,20 @@
-(* Title: HOL/lfp.thy
+(* Title: CCL/Lfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
-The Knaster-Tarski Theorem
*)
-Lfp = Set +
-consts lfp :: "['a set=>'a set] => 'a set"
-rules
- (*least fixed point*)
- lfp_def "lfp(f) == Inter({u. f(u) <= u})"
+header {* The Knaster-Tarski Theorem *}
+
+theory Lfp
+imports Set
+uses "subset.ML" "equalities.ML" "mono.ML"
+begin
+
+constdefs
+ lfp :: "['a set=>'a set] => 'a set" (*least fixed point*)
+ "lfp(f) == Inter({u. f(u) <= u})"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end