src/HOL/Probability/Finite_Product_Measure.thy

--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -11,9 +11,6 @@
 lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
   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
-
 abbreviation
   "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"