# HG changeset patch
# User blanchet
# Date 1409695189 -7200
# Node ID 00c878bd20934a8a6af8fd70e6ac20797aca3c76
# Parent  7f7026ae9dc5a3df67f2e0f84ff76cca62a48de1
removed more slow Refute tests

diff -r 7f7026ae9dc5 -r 00c878bd2093 src/HOL/ex/Refute_Examples.thy
--- 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 *}