--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 29 14:27:31 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Mar 29 14:27:39 2011 +0200
@@ -6,7 +6,7 @@
header {* Lebsegue measure *}
theory Lebesgue_Measure
- imports Product_Measure
+ imports Finite_Product_Measure
begin
subsection {* Standard Cubes *}
@@ -50,9 +50,6 @@
lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
-lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
- unfolding Pi_def by auto
-
subsection {* Lebesgue measure *}
definition lebesgue :: "'a::ordered_euclidean_space measure_space" where