author | noschinl |
Fri, 16 Sep 2011 20:08:29 +0200 | |
changeset 44941 | 617eb31e63f9 |
parent 44940 | 56fd289398a2 |
child 44943 | b62559f085bc |
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Sep 16 20:02:35 2011 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Sep 16 20:08:29 2011 +0200 @@ -412,7 +412,6 @@ proof (rule antisym) show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y" using g_in_G - using [[simp_trace]] by (auto intro!: exI Sup_mono simp: SUP_def) show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq by (auto intro!: SUP_mono positive_integral_mono Max_ge)