--- a/src/HOL/BNF_Def.thy Wed Jan 29 15:05:53 2014 +0100
+++ b/src/HOL/BNF_Def.thy Wed Jan 29 16:35:05 2014 +0100
@@ -110,10 +110,11 @@
by auto
lemma Collect_split_mono_strong:
- "\<lbrakk>\<forall>a\<in>fst ` A. \<forall>b \<in> snd ` A. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
+ "\<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 (split P)\<rbrakk> \<Longrightarrow>
A \<subseteq> Collect (split Q)"
by fastforce
+
lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
by metis