# HG changeset patch
# User skalberg
# Date 1062000839 -7200
# Node ID 0590de71a016eb8f04254f59f6aa6626efdc6939
# Parent  ed81cd283816e2f46cdc002a2266b35a1e7aa568
Converted to new style theories.

diff -r ed81cd283816 -r 0590de71a016 src/HOL/Gfp.ML
--- a/src/HOL/Gfp.ML	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Gfp.ML	Wed Aug 27 18:13:59 2003 +0200
@@ -8,6 +8,8 @@
 
 (*** Proof of Knaster-Tarski Theorem using gfp ***)
 
+val gfp_def = thm "gfp_def";
+
 (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
 
 Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
diff -r ed81cd283816 -r 0590de71a016 src/HOL/Gfp.thy
--- a/src/HOL/Gfp.thy	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Gfp.thy	Wed Aug 27 18:13:59 2003 +0200
@@ -6,10 +6,10 @@
 Greatest fixed points (requires Lfp too!)
 *)
 
-Gfp = Lfp +
+theory Gfp = Lfp:
 
 constdefs
-  gfp :: ['a set=>'a set] => 'a set
+  gfp :: "['a set=>'a set] => 'a set"
   "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
 
 end
diff -r ed81cd283816 -r 0590de71a016 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Lfp.ML	Wed Aug 27 18:13:59 2003 +0200
@@ -8,6 +8,8 @@
 
 (*** Proof of Knaster-Tarski Theorem ***)
 
+val lfp_def = thm "lfp_def";
+
 (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
 
 Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";
diff -r ed81cd283816 -r 0590de71a016 src/HOL/Lfp.thy
--- a/src/HOL/Lfp.thy	Wed Aug 27 18:13:39 2003 +0200
+++ b/src/HOL/Lfp.thy	Wed Aug 27 18:13:59 2003 +0200
@@ -6,10 +6,10 @@
 The Knaster-Tarski Theorem
 *)
 
-Lfp = Product_Type +
+theory Lfp = Product_Type:
 
 constdefs
-  lfp :: ['a set=>'a set] => 'a set
+  lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
 
 end