diff -r e0825405d398 -r 0dfcd0fb4172 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Mon Oct 12 22:03:24 2015 +0200
+++ b/src/HOL/BNF_Def.thy	Tue Oct 13 09:21:14 2015 +0200
@@ -176,15 +176,6 @@
 lemma flip_pred: "A \<subseteq> Collect (case_prod (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (case_prod R)"
   by auto
 
-lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
-  by auto
-
-lemma Collect_split_mono_strong: 
-  "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (case_prod P)\<rbrakk> \<Longrightarrow>
-   A \<subseteq> Collect (case_prod Q)"
-  by fastforce
-
-
 lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
   by simp