# HG changeset patch
# User hoelzl
# Date 1353073583 -3600
# Node ID 9af8721ecd20e6128c3896c365bc86dcb3dd465e
# Parent  a58bb401af80ae0ef2a86ab3be4489ce4c63d1c9
renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose

diff -r a58bb401af80 -r 9af8721ecd20 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Nov 16 14:46:23 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Nov 16 14:46:23 2012 +0100
@@ -1278,7 +1278,7 @@
 subsection {* Isomorphism between Functions and Finite Maps *}
 
 lemma
-  measurable_compose:
+  measurable_finmap_compose:
   fixes f::"'a \<Rightarrow> 'b"
   assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j"
   assumes "finite J"
@@ -1326,7 +1326,7 @@
   shows "(\<lambda>m. compose (f ` J) m f') \<in> measurable (PiM J (\<lambda>_. M)) (PiM (f ` J) (\<lambda>_. M))"
 proof -
   have "(\<lambda>m. compose (f ` J) m f') \<in> measurable (Pi\<^isub>M (f' ` f ` J) (\<lambda>_. M)) (Pi\<^isub>M (f ` J) (\<lambda>_. M))"
-    using assms by (auto intro: measurable_compose)
+    using assms by (auto intro: measurable_finmap_compose)
   moreover
   from inj have "f' ` f ` J = J" by (metis (hide_lams, mono_tags) image_iff set_eqI)
   ultimately show ?thesis by simp
@@ -1426,7 +1426,7 @@
 proof (rule measurable_comp, rule measurable_proj_PiM)
   show "(\<lambda>g. compose J g f) \<in>
     measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))"
-    by (rule measurable_compose, rule inv) auto
+    by (rule measurable_finmap_compose, rule inv) auto
 qed (auto simp add: space_PiM extensional_def assms)
 
 lemma fm_image_measurable: