src/HOL/Probability/Distributions.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 58709 efdc6c533bd3
--- a/src/HOL/Probability/Distributions.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -33,7 +33,7 @@
     by (auto simp add: field_simps)
 
   have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
-    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
+    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
     
   have "density lborel f = distr M lborel X"
     using f by (simp add: distributed_def)
@@ -49,7 +49,7 @@
   shows "distributed M lborel X f"
 proof -
   have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
-    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
+    using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
 
   show ?thesis
     using distributed_affine[OF f c, where t=t] c