src/HOL/Probability/Distributions.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58709 efdc6c533bd3
```     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
```