src/HOL/Probability/Binary_Product_Measure.thy
changeset 50002 ce0d316b5b44
parent 49999 dfb63b9b8908
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 02 14:23:40 2012 +0100
     1.3 @@ -100,7 +100,9 @@
     1.4  
     1.5  lemma measurable_pair_iff:
     1.6    "f \<in> measurable M (M1 \<Otimes>\<^isub>M M2) \<longleftrightarrow> (fst \<circ> f) \<in> measurable M M1 \<and> (snd \<circ> f) \<in> measurable M M2"
     1.7 -  using measurable_pair[of f M M1 M2] by auto
     1.8 +  using measurable_pair[of f M M1 M2]
     1.9 +  using [[simproc del: measurable]] (* the measurable method is nonterminating when using measurable_pair *)
    1.10 +  by auto
    1.11  
    1.12  lemma measurable_split_conv:
    1.13    "(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"