--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Oct 17 07:50:46 2018 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed Oct 17 14:19:07 2018 +0100
@@ -2853,8 +2853,6 @@
by (simp cong: measurable_cong)
qed
-lemma%unimportant Collect_subset [simp]: "{x\<in>A. P x} \<subseteq> A" by auto
-
lemma%unimportant (in sigma_finite_measure) measurable_measure[measurable (raw)]:
"(\<And>x. x \<in> space N \<Longrightarrow> A x \<subseteq> space M) \<Longrightarrow>
{x \<in> space (N \<Otimes>\<^sub>M M). snd x \<in> A (fst x)} \<in> sets (N \<Otimes>\<^sub>M M) \<Longrightarrow>