--- a/src/HOL/BNF_Greatest_Fixpoint.thy Thu Aug 27 13:07:45 2015 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Thu Aug 27 21:19:48 2015 +0200
@@ -82,13 +82,13 @@
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
by blast
-lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
+lemma in_rel_Collect_split_eq: "in_rel (Collect (case_prod X)) = X"
unfolding fun_eq_iff by auto
-lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
+lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (case_prod (in_rel Y))"
by auto
-lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
+lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (case_prod (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
by force
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"