--- 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)"