diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Thu Nov 15 14:04:23 2012 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Thu Nov 15 10:49:58 2012 +0100
@@ -8,20 +8,6 @@
   imports Probability_Measure Infinite_Product_Measure
 begin
 
-lemma INT_decseq_offset:
-  assumes "decseq F"
-  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
-proof safe
-  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
-  show "x \<in> F i"
-  proof cases
-    from x have "x \<in> F n" by auto
-    also assume "i \<le> n" with `decseq F` have "F n \<subseteq> F i"
-      unfolding decseq_def by simp
-    finally show ?thesis .
-  qed (insert x, simp)
-qed auto
-
 definition (in prob_space)
   "indep_sets F I \<longleftrightarrow> (\<forall>i\<in>I. F i \<subseteq> events) \<and>
     (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> (\<forall>A\<in>Pi J F. prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))))"