removed a refute example that caused trouble with testing
authorblanchet
Thu, 09 Apr 2015 18:00:59 +0200
changeset 59987 fbe93138e540
parent 59986 f38b94549dc8
child 59988 c92afea6eb4b
removed a refute example that caused trouble with testing
src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Apr 09 18:00:58 2015 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Apr 09 18:00:59 2015 +0200
@@ -259,15 +259,6 @@
 refute [expect = genuine]
 oops
 
-text {* "The union of transitive closures is equal to the transitive closure of unions." *}
-
-lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
-        \<longrightarrow> trans_closure TP P
-        \<longrightarrow> trans_closure TR R
-        \<longrightarrow> (T x y = (TP x y | TR x y))"
-refute [expect = genuine]
-oops
-
 text {* "Every surjective function is invertible." *}
 
 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"