--- a/src/HOL/ex/Refute_Examples.thy Tue Sep 02 23:59:46 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Tue Sep 02 23:59:49 2014 +0200
@@ -1266,18 +1266,6 @@
refute [expect = potential]
oops
-lemma "f (lfp f) = lfp f"
-refute [expect = genuine]
-oops
-
-lemma "f (gfp f) = gfp f"
-refute [expect = genuine]
-oops
-
-lemma "lfp f = gfp f"
-refute [expect = genuine]
-oops
-
(*****************************************************************************)
subsubsection {* Type classes and overloading *}