1.1 --- a/src/HOL/Probability/Distributions.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Probability/Distributions.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4      by (auto simp add: field_simps)
     1.5  
     1.6    have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
     1.7 -    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
     1.8 +    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
     1.9      
    1.10    have "density lborel f = distr M lborel X"
    1.11      using f by (simp add: distributed_def)
    1.12 @@ -49,7 +49,7 @@
    1.13    shows "distributed M lborel X f"
    1.14  proof -
    1.15    have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
    1.16 -    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
    1.17 +    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
    1.18  
    1.19    show ?thesis
    1.20      using distributed_affine[OF f c, where t=t] c