src/HOL/Probability/Radon_Nikodym.thy
changeset 56166 9a241bc276cd
parent 55642 63beb38e9258
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -386,7 +386,7 @@
     1.4    also have "\<dots> = ?y"
     1.5    proof (rule antisym)
     1.6      show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
     1.7 -      using g_in_G by (auto intro: Sup_mono simp: SUP_def)
     1.8 +      using g_in_G by (auto intro: SUP_mono)
     1.9      show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
    1.10        by (auto intro!: SUP_mono positive_integral_mono Max_ge)
    1.11    qed