diff -r 9bfb016cb35e -r 828fc32f390f src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Mon May 23 16:57:02 2005 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Mon May 23 17:17:06 2005 +0200
@@ -901,8 +901,6 @@
 
 subsection {* Inductively defined sets *}
 
-(*TODO: can we implement lfp/gfp more efficiently? *)
-
 consts
   arbitrarySet :: "'a set"
 inductive arbitrarySet
@@ -910,7 +908,7 @@
   "arbitrary : arbitrarySet"
 
 lemma "x : arbitrarySet"
-  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
+  refute
 oops
 
 consts
@@ -921,7 +919,7 @@
   "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
 
 lemma "S : evenCard"
-  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
+  refute
 oops
 
 consts
@@ -934,7 +932,7 @@
   "n : odd \<Longrightarrow> Suc n : even"
 
 lemma "n : odd"
-  (*TODO refute*)  -- {* unfortunately, this little example already takes too long *}
+  (*refute*)  -- {* unfortunately, this little example already takes too long *}
 oops
 
 (******************************************************************************)
@@ -977,6 +975,18 @@
   refute
 oops
 
+lemma "f (lfp f) = lfp f"
+  refute
+oops
+
+lemma "f (gfp f) = gfp f"
+  refute
+oops
+
+lemma "lfp f = gfp f"
+  refute
+oops
+
 (******************************************************************************)
 
 subsection {* Axiomatic type classes and overloading *}