Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Probability/Distributions.thy
changeset 57512 cc97b347b301
parent 57447 87429bdecad5
child 57514 bdc2c6b40bf2 
     1.1 --- a/src/HOL/Probability/Distributions.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Probability/Distributions.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -865,7 +865,7 @@
     1.4      proof (subst nn_integral_FTC_atLeast)
     1.5        have "((\<lambda>a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) ---> (- (0 / (2 + 2 * s\<^sup>2)))) at_top"
     1.6          apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top])
     1.7 -        apply (subst mult_commute)         
     1.8 +        apply (subst mult.commute)         
     1.9          apply (auto intro!: filterlim_tendsto_pos_mult_at_top
    1.10                              filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] 
    1.11                      simp: add_pos_nonneg  power2_eq_square add_nonneg_eq_0_iff)
isabelle