1.1 --- a/src/HOL/Gfp.ML	Wed Aug 27 18:13:39 2003 +0200
     1.2 +++ b/src/HOL/Gfp.ML	Wed Aug 27 18:13:59 2003 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  (*** Proof of Knaster-Tarski Theorem using gfp ***)
     1.6  
     1.7 +val gfp_def = thm "gfp_def";
     1.8 +
     1.9  (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
    1.10  
    1.11  Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";

     2.1 --- a/src/HOL/Gfp.thy	Wed Aug 27 18:13:39 2003 +0200
     2.2 +++ b/src/HOL/Gfp.thy	Wed Aug 27 18:13:59 2003 +0200
     2.3 @@ -6,10 +6,10 @@
     2.4  Greatest fixed points (requires Lfp too!)
     2.5  *)
     2.6  
     2.7 -Gfp = Lfp +
     2.8 +theory Gfp = Lfp:
     2.9  
    2.10  constdefs
    2.11 -  gfp :: ['a set=>'a set] => 'a set
    2.12 +  gfp :: "['a set=>'a set] => 'a set"
    2.13    "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
    2.14  
    2.15  end

     3.1 --- a/src/HOL/Lfp.ML	Wed Aug 27 18:13:39 2003 +0200
     3.2 +++ b/src/HOL/Lfp.ML	Wed Aug 27 18:13:59 2003 +0200
     3.3 @@ -8,6 +8,8 @@
     3.4  
     3.5  (*** Proof of Knaster-Tarski Theorem ***)
     3.6  
     3.7 +val lfp_def = thm "lfp_def";
     3.8 +
     3.9  (* lfp(f) is the greatest lower bound of {u. f(u) <= u} *)
    3.10  
    3.11  Goalw [lfp_def] "f(A) <= A ==> lfp(f) <= A";

     4.1 --- a/src/HOL/Lfp.thy	Wed Aug 27 18:13:39 2003 +0200
     4.2 +++ b/src/HOL/Lfp.thy	Wed Aug 27 18:13:59 2003 +0200
     4.3 @@ -6,10 +6,10 @@
     4.4  The Knaster-Tarski Theorem
     4.5  *)
     4.6  
     4.7 -Lfp = Product_Type +
     4.8 +theory Lfp = Product_Type:
     4.9  
    4.10  constdefs
    4.11 -  lfp :: ['a set=>'a set] => 'a set
    4.12 +  lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
    4.13    "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
    4.14  
    4.15  end