--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Nov 15 10:49:58 2012 +0100
@@ -1161,9 +1161,6 @@
by (intro sigma_sets_subset) (auto simp: E_generates sets_Collect_single)
qed
-lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
- by metis
-
lemma sigma_prod_algebra_sigma_eq:
fixes E :: "'i \<Rightarrow> 'a set set" and S :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
assumes "finite I"