# HG changeset patch
# User noschinl
# Date 1316196509 -7200
# Node ID 617eb31e63f90006817db7ca743112161bb52d2e
# Parent  56fd289398a2792b4a850cc8f6ea5ffb0ab4ce79
remove stray "using [[simp_trace]]"

diff -r 56fd289398a2 -r 617eb31e63f9 src/HOL/Probability/Radon_Nikodym.thy
--- 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)