src/HOL/Probability/Probability_Mass_Function.thy
changeset 62390 842917225d56
parent 62324 ae44f16dcea5
child 62975 1d066f6ab25d
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -876,7 +876,7 @@
     1.4    by transfer (simp add: emeasure_measure_pmf_not_zero pmf.rep_eq)
     1.5  
     1.6  lemma set_cond_pmf[simp]: "set_pmf cond_pmf = set_pmf p \<inter> s"
     1.7 -  by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: split_if_asm)
     1.8 +  by (auto simp add: set_pmf_iff pmf_cond measure_measure_pmf_not_zero split: if_split_asm)
     1.9  
    1.10  end
    1.11