remove stray "using [[simp_trace]]"
authornoschinl
Fri Sep 16 20:08:29 2011 +0200 (2011-09-16)
changeset 44941617eb31e63f9
parent 44940 56fd289398a2
child 44943 b62559f085bc
remove stray "using [[simp_trace]]"
src/HOL/Probability/Radon_Nikodym.thy
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Sep 16 20:02:35 2011 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Sep 16 20:08:29 2011 +0200
     1.3 @@ -412,7 +412,6 @@
     1.4    proof (rule antisym)
     1.5      show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y"
     1.6        using g_in_G
     1.7 -      using [[simp_trace]]
     1.8        by (auto intro!: exI Sup_mono simp: SUP_def)
     1.9      show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq
    1.10        by (auto intro!: SUP_mono positive_integral_mono Max_ge)