# HG changeset patch
# User hoelzl
# Date 1335359219 -7200
# Node ID 7b2836a43cc9504e23afc49bf113c4f89c216804
# Parent  df437d1bf8db90dff6da070ab00595ce1433e188
correct lemma name

diff -r df437d1bf8db -r 7b2836a43cc9 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Apr 25 14:33:21 2012 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Apr 25 15:06:59 2012 +0200
@@ -877,7 +877,7 @@
   "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
   by (auto intro!: sigma_sets_subseteq)
 
-lemma in_extended_measure[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
+lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
   by auto
 
 section {* Constructing simple @{typ "'a measure"} *}
@@ -1029,7 +1029,7 @@
 lemma measurable_iff_measure_of:
   assumes "N \<subseteq> Pow \<Omega>" "f \<in> space M \<rightarrow> \<Omega>"
   shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)"
-  by (metis assms in_extended_measure measurable_measure_of assms measurable_sets)
+  by (metis assms in_measure_of measurable_measure_of assms measurable_sets)
 
 lemma measurable_cong:
   assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"